search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
585 stars 237 forks source link

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

Closed jamesmckinna closed 1 month ago

jamesmckinna commented 1 month ago

Fixes #2482 (I hope).

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

jamesmckinna commented 1 month ago

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 commented 1 month ago

Sure

jamesmckinna commented 1 month ago

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 commented 1 month ago

Merging in as @JacquesCarette has already approved.