Skip to content

Properties of Pseudolattice#1272

Merged
mortberg merged 8 commits intoagda:masterfrom
LorenzoMolena:pseudolattice-properties
Feb 17, 2026
Merged

Properties of Pseudolattice#1272
mortberg merged 8 commits intoagda:masterfrom
LorenzoMolena:pseudolattice-properties

Conversation

@LorenzoMolena
Copy link
Contributor

Update to the Pseudolattice module.
It introduces the definition of equivalences between pseudolattices, following the pattern used in the other order structures, and adds a basic Properties module containing the results that seem most generally useful.

@LorenzoMolena
Copy link
Contributor Author

@mortberg @ecavallo @mzeuner I was wondering whether this PR and #1271 might be reviewed when convenient.
They have been open for a few months, and reviewing them would help with the ongoing development of fast Integers as well as some upcoming work on the OCR structure of Rationals and Reals.
Many thanks in advance!

@mortberg
Copy link
Collaborator

This also looks good to me, except for the conflict. Can you fix the conflict and ping me again and I'll merge it?

@LorenzoMolena
Copy link
Contributor Author

@mortberg I fixed the conflicts

@mortberg mortberg merged commit 04cc7d9 into agda:master Feb 17, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants

Comments