`Fast.Int` Update#1280

Open

LorenzoMolena wants to merge 11 commits intoagda:masterfrom

LorenzoMolena:fast-int-update-without-order

Commits on Nov 19, 2025

Fast int properties with pl and ocr instances (#23)

authored

Commits on Nov 22, 2025

edit `zero-≤pos`, using an easier proof, add `zero-<possuc`
LorenzoMolena
committed

Commits on Dec 13, 2025

remove `Int.Fast.Order` and related instances ; merge properties of Pseudolattices and simplify some proofs about min/max in `Int.Fast.Properties`
LorenzoMolena
committed
move `Fast` Integer files to `Fast` folder, and similarly for the algebraic instances
LorenzoMolena
committed
rename the algebraic instances of fast integers
LorenzoMolena
committed
another rename
LorenzoMolena
committed
fix imports, remove unnecessary code in `Pseudolattice.Properties`
LorenzoMolena
committed
Merge branch 'agda:master' into fast-int-update-without-order
LorenzoMolena
authored
remove `Ordering` data type (I'll leave it for the PR with fast integer order)
LorenzoMolena
committed

Commits on Jan 24, 2026