Skip to content

Data.Nat.Base is missing raw algebra bundles involving multiplication #1858

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
Closed
Taneb opened this issue Oct 24, 2022 · 4 comments · Fixed by #1861
Closed

Data.Nat.Base is missing raw algebra bundles involving multiplication #1858

Taneb opened this issue Oct 24, 2022 · 4 comments · Fixed by #1861
Labels
addition

Comments

@Taneb
Copy link
Member

Taneb commented Oct 24, 2022

  • *-rawMagma
  • *-1-rawMonoid
  • +-*-rawNearSemiring
  • +-*-rawSemiring
@jamesmckinna
Copy link
Contributor

Suggest I add these to the Parity PR #1852 (arrogantly presuming that mention of these omissions was prompted by those additions...)?

@MatthewDaggitt
Copy link
Contributor

MatthewDaggitt commented Oct 24, 2022 •
edited
Loading

Nope, definitely open a separate PR! No need to wrap them up in the same one 👍 They're not related, so no need for them to go in the same PR.

@jamesmckinna
Copy link
Contributor

OK, but I will move the raw bundles from Data.Parity.Properties to Base.

jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this issue Oct 24, 2022
@jamesmckinna
[fix] added raw bundles (agda#1858)
71efef8
This was linked to pull requests Oct 24, 2022
Resolves issue #509 and resolves issue #626 #1822
Merged
[fix] added raw bundles to Data.Nat.Base #1861
Merged
@jamesmckinna jamesmckinna removed a link to a pull request Oct 24, 2022
Resolves issue #509 and resolves issue #626 #1822
Merged
4 tasks
@jamesmckinna
Copy link
Contributor

jamesmckinna commented Oct 24, 2022 •
edited
Loading

Erroneous linkage to PR #1822 which I now don't seem able to unlink... :-( or else it leaves a trail. Oh well... careless mouse handling!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
addition
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

[fix] added raw bundles to Data.Nat.Base jamesmckinna/agda-stdlib
3 participants
@Taneb @MatthewDaggitt @jamesmckinna