Skip to content

parity is a Semiring homomorphism #1894

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 16 commits into from
Jan 9, 2023
Merged

parity is a Semiring homomorphism #1894

merged 16 commits into from
Jan 9, 2023

Conversation

jamesmckinna
Copy link
Contributor

This PR follows up on the earlier #1852, and in the absence of any satisfactory resolution of issue #1871, makes the choice to put this under Data.Parity, moreover with an ugly/improvable module name. Suggestions welcome!

@jamesmckinna
Copy link
Contributor Author

Re: CHANGELOG
Should I add simply the final lemma, or all the new definitions, or simply the new module (name) to the log?

MatthewDaggitt
MatthewDaggitt reviewed Dec 30, 2022
View reviewed changes
@MatthewDaggitt MatthewDaggitt added this to the v2.0 milestone Dec 30, 2022
@MatthewDaggitt
Copy link
Contributor

And of course a CHANGELOG entry would be great 👍

JacquesCarette
JacquesCarette reviewed Dec 30, 2022
View reviewed changes
Copy link
Contributor

@JacquesCarette JacquesCarette left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm quite happy with these things being defined where they are. These are things that are quite special to the relationship between Nat and parity.

Any reason for all the Effect changes to be here? Some errant merge?

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Dec 30, 2022 •
edited
Loading

And yes, an errant merge. Blast. Pause while I roll everything back again and re-commit. Grrr.

@JacquesCarette
Copy link
Contributor

Things are looking great. Except that you seem to have lost your CHANGELOG changes while fixing the errant merge.

@jamesmckinna
Copy link
Contributor Author

Things are looking great. Except that you seem to have lost your CHANGELOG changes while fixing the errant merge.

Fixed now?

@JacquesCarette
Copy link
Contributor

Yes, everything's looking good now.

@MatthewDaggitt MatthewDaggitt merged commit 1a9d334 into agda:master Jan 9, 2023
@jamesmckinna jamesmckinna deleted the parity-bis branch January 9, 2023 15:44
MatthewDaggitt added a commit that referenced this pull request Jan 10, 2023
@MatthewDaggitt
Revert "parity is a Semiring homomorphism (#1894)"
90c2deb 
This reverts commit 1a9d334.
@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Jan 10, 2023 •
edited
Loading

OK, checked out a clean branch (but maybe from the wrong base?), but the associated PR doesn't look right... Now try again with PR #1904

@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

@JacquesCarette JacquesCarette JacquesCarette left review comments

@MatthewDaggitt MatthewDaggitt MatthewDaggitt left review comments

Assignees
No one assigned
Labels
addition
Projects
None yet
Milestone
v2.0
Development

Successfully merging this pull request may close these issues.
3 participants
@jamesmckinna @MatthewDaggitt @JacquesCarette