Skip to content

Add Monoid for Add Point (#845) #1751

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.

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

Merged
merged 2 commits into from
Jul 14, 2022
Merged

Conversation

Boarders
Copy link
Contributor

Adds Monoid for Pointed and also adds an idempotent proof for <∣>.

Note: I don't know the standard library very well (nor much module-fu) so please feel free to make suggestions for improvements.

Copy link
Contributor

@MatthewDaggitt MatthewDaggitt left a comment

Choose a reason for hiding this comment

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

Thank you for the great first PR, we really appreciate it! Just a heads-up that this isn't the easiest low-hanging-fruit on the tree, so it might require a couple of review iterations 😅

I've started off with the most important points and we can go from there.

@Boarders
Copy link
Contributor Author

Have another draft of this attempting to address your points so far @MatthewDaggitt .

Copy link
Contributor

@MatthewDaggitt MatthewDaggitt left a comment

Choose a reason for hiding this comment

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

Thanks, here are a few more!

@Boarders
Copy link
Contributor Author

Have another draft whenever you have the time @MatthewDaggitt

Copy link
Contributor

@MatthewDaggitt MatthewDaggitt left a comment

Choose a reason for hiding this comment

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

Thanks. Here's the final(?) batch.

You will also need to an entry in the CHANGELOG.md file the top level describing the changes. One entry in the new modules section, and one entry in the minor changes section.

@Boarders Boarders force-pushed the monoids branch 2 times, most recently from a012ddb to df62ebe Compare April 17, 2022 16:11
@Boarders
Copy link
Contributor Author

Updated with the suggested improvements.

Copy link
Contributor

@MatthewDaggitt MatthewDaggitt left a comment

Choose a reason for hiding this comment

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

Thanks! Apologies I've found a few more small points, but then it really is finished, promise!

@Boarders
Copy link
Contributor Author

Boarders commented May 2, 2022

Life got in the way of this, will make these changes this week!

@MatthewDaggitt
Copy link
Contributor

@Boarders any prospect of you finding the time to make the last tweaks so I can merge this in?

@Boarders
Copy link
Contributor Author

Boarders commented Jul 1, 2022

Ah apologies, this completely slipped off my radar. Should be able to get these changes to you today!

@Boarders
Copy link
Contributor Author

Boarders commented Jul 3, 2022

I made these changes but let me know if you don't like the style of naming I introduced and I'm happy to change it or anything else I overlooked. Thank you for such through reviewing and apologies for the delay.

@MatthewDaggitt
Copy link
Contributor

Looks great! As soon as the tests pass I'll merge it in 👍 Thanks for the PR!

@MatthewDaggitt MatthewDaggitt merged commit 1aa9865 into agda:master Jul 14, 2022
@andreasabel andreasabel mentioned this pull request Aug 27, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants