Skip to content

[fix] added raw bundles to Data.Nat.Base #1861

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 5 commits into from
Oct 25, 2022
Merged

[fix] added raw bundles to Data.Nat.Base #1861

merged 5 commits into from
Oct 25, 2022

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Oct 24, 2022 •
edited
Loading

EDITED: Removed duplicate bundles, so should be fixed now.
DONE: update CHANGELOG to record new bundles added

@jamesmckinna jamesmckinna changed the title [fix] added raw bundles to Data.Nat.Base ([agda#1858](https://github.com/agda/agda-stdlib/issues/1858)) [fix] added raw bundles to Data.Nat.Base Oct 24, 2022
@jamesmckinna jamesmckinna mentioned this pull request Oct 24, 2022
Closed
@jamesmckinna jamesmckinna linked an issue Oct 24, 2022 that may be closed by this pull request
Data.Nat.Base is missing raw algebra bundles involving multiplication #1858
Closed
@MatthewDaggitt MatthewDaggitt added this to the v2.0 milestone Oct 25, 2022
@MatthewDaggitt MatthewDaggitt merged commit 88942c3 into agda:master Oct 25, 2022
@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Oct 25, 2022 •
edited
Loading

I had thought I'd tidy up after myself with addressing issue #1865 , but perhaps that can now wait for a subsequent PR?
What's the preferred workflow? Have continued to push commits to this branch...

@JacquesCarette
Copy link
Contributor

Oh no, I blinked and missed this... I really don't think it's a good idea to have large .Base. .Base should just define the operations and nothing else. I hate having .Base depend on anything in Algebra. I really think all these bundles should be in Data.Nat.Bundles (or Data.Nat.RawBundles).

@andreasabel andreasabel mentioned this pull request Jul 24, 2023
Merged
@andreasabel andreasabel mentioned this pull request Aug 27, 2023
Merged
@andreasabel andreasabel mentioned this pull request Oct 12, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
addition
Projects
None yet
Milestone
v2.0
Development

Successfully merging this pull request may close these issues.

Data.Nat.Base is missing raw algebra bundles involving multiplication
3 participants
@jamesmckinna @JacquesCarette @MatthewDaggitt