Comm ring solver improvement#1293

Draft

marcinjangrzybowski wants to merge 36 commits into

agda:masterfrom

marcinjangrzybowski:comm-ring-solver-improvments

Commits on Sep 18, 2025

Add commutative ring and field instances for `Data.Rationals`
broughjt
committed

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

Commits on Feb 14, 2026

Commits on Feb 17, 2026

Commits on Feb 20, 2026

wip
marcinjangrzybowski
committed

Commits on Feb 22, 2026

wip
marcinjangrzybowski
committed

Commits on Feb 24, 2026

wip
marcinjangrzybowski
committed

Commits on Feb 28, 2026

wip
marcinjangrzybowski
committed

Commits on Mar 6, 2026

wip
marcinjangrzybowski
committed

Commits on Mar 14, 2026

wip
marcinjangrzybowski
committed

Commits on Mar 24, 2026

compiles
marcinjangrzybowski
committed

Commits on Mar 27, 2026

works
marcinjangrzybowski
committed

Commits on Mar 28, 2026

Commits on Mar 29, 2026

wip, reshufling solver modules
marcinjangrzybowski
committed