feat: Numbers#67

Merged

markusdemedeiros merged 25 commits intoleanprover-community:masterfrom

Shreyas4991:numbers

Jan 23, 2026

Commits on Jun 22, 2025

feat: implement frac
markusdemedeiros
committed

Commits on Jun 24, 2025

Ordered Commutative Monoids are more useful for numbers. Fracs should be modelled as dyadic rationals. see Mario's suggestion
Shreyas4991
committed

Commits on Jun 30, 2025

Commits on Jul 1, 2025

Fix copyright header
Shreyas4991
committed

Commits on Jul 2, 2025

Fixed API lemmas. allows negative numbers now. Next, fix the CMRA instance
Shreyas4991
committed

Commits on Jul 8, 2025

Commits on Jul 18, 2025

Commits on Aug 13, 2025

Update numbers
Shreyas4991
committed

Commits on Jan 23, 2026