Skip to content

Properties of Pseudolattice - #1272

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

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

Conversation

@LorenzoMolena

Copy link
Copy Markdown
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 LorenzoMolena mentioned this pull request Dec 16, 2025
@LorenzoMolena

Copy link
Copy Markdown
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
Copy Markdown
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
Copy Markdown
Contributor Author

@mortberg I fixed the conflicts

@mortberg
mortberg merged commit 04cc7d9 into agda:master Feb 17, 2026
1 check passed
@LorenzoMolena
LorenzoMolena deleted the pseudolattice-properties branch April 3, 2026 12:04
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