Skip to content
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

Add (Is)DecPreorder to Relation.Binary.* #2488

Merged
merged 5 commits into from
Oct 7, 2024
Merged

Add (Is)DecPreorder to Relation.Binary.* #2488

merged 5 commits into from
Oct 7, 2024

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Sep 27, 2024 •
edited
Loading

Fixes #2482 (I hope).

UPDATED: DONE knock-on consequences for #2481 ... which prompted these additions in the first place!

MatthewDaggitt
MatthewDaggitt reviewed Sep 28, 2024
View reviewed changes
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.

Do we need to construct the DecPreorder objects in the other higher Dec bundles?

Otherwise, looks good!

@MatthewDaggitt MatthewDaggitt added this to the v2.2 milestone Sep 28, 2024
@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Sep 28, 2024 •
edited
Loading

Do we need to construct the DecPreorder objects in the other higher Dec bundles?

Sigh... yes, we should. I haven't done one of these 'structural' PRs for a while... and they do give me a bit of a headache (eg wrt the renaming directives in the reexport of isPreorder in IsPartialOrder etc.). Maybe make this a downstream PR?

UPDATED: latest commit attempts to add the additional fields... another set of eyes would be helpful!

@MatthewDaggitt
Copy link
Contributor

Sure

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Sep 30, 2024 •
edited
Loading

So I think the Structures story is OK, but the Bundles definitely need refactoring as regards their module Eq and decSetoid definitions are concerned. I'll take a look later tomorrow...

... UPDATED: tomorrow becomes today, and I think I've now finished my tasks. I'd welcome a re-review just to check, however!

MatthewDaggitt
MatthewDaggitt approved these changes Oct 7, 2024
View reviewed changes
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.

This all looks good! Nice job on the inheritance!

@MatthewDaggitt
Copy link
Contributor

Merging in as @JacquesCarette has already approved.

@MatthewDaggitt MatthewDaggitt added this pull request to the merge queue Oct 7, 2024
Merged via the queue into agda:master with commit 6078b64 Oct 7, 2024
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@MatthewDaggitt MatthewDaggitt MatthewDaggitt approved these changes

@JacquesCarette JacquesCarette Awaiting requested review from JacquesCarette

Assignees
No one assigned
Labels
addition low-hanging-fruit
Projects
None yet
Milestone
v2.2
Development

Successfully merging this pull request may close these issues.

Missing structure/bundle in the Relation.Binary.* hierarchy?
3 participants
@jamesmckinna @MatthewDaggitt @JacquesCarette