feat: Views#60

Closed

markusdemedeiros wants to merge 58 commits intomasterfrom

Commits on Jul 1, 2025

Add prod and unit CMRAs

suhr
authored and
markusdemedeiros
committed
fix: add back in validity lemmas
markusdemedeiros
committed
fix: Prod namespace
markusdemedeiros
committed
fix: remove warnings
markusdemedeiros
committed
Add Local Updates

suhr
authored and
markusdemedeiros
committed
fix: naming and style

oliversoeser
authored and
markusdemedeiros
committed
Add Updates

suhr
authored and
markusdemedeiros
committed
fix: naming and sections

oliversoeser
authored and
markusdemedeiros
committed
feat: implement frac
markusdemedeiros
committed
Initial comit

Shreyas4991
authored and
markusdemedeiros
committed
Add positive lemma. Why are all the instances failing now

Shreyas4991
authored and
markusdemedeiros
committed
Add halving axiom

Shreyas4991
authored and
markusdemedeiros
committed
Remove halving

Shreyas4991
authored and
markusdemedeiros
committed
one sorry down

Shreyas4991
authored and
markusdemedeiros
committed
two sorries down

Shreyas4991
authored and
markusdemedeiros
committed
Narrow down error

Shreyas4991
authored and
markusdemedeiros
committed
Narrow down error

Shreyas4991
authored and
markusdemedeiros
committed
Turn all non-terminal simps into simp onlys

Shreyas4991
authored and
markusdemedeiros
committed
Add name to authors list

Shreyas4991
authored and
markusdemedeiros
committed
factor out the <1 features
markusdemedeiros
committed
Fractor out UFractional
markusdemedeiros
committed
tweak Fractional and Whole definition
markusdemedeiros
committed
more Frac lemmas
markusdemedeiros
committed
Relax UFraction typeclass
markusdemedeiros
committed
feat: implement dfrac
markusdemedeiros
committed
sorry out breaking changes
markusdemedeiros
committed
Update DFractional to alias UFractional
markusdemedeiros
committed
checkpoint
markusdemedeiros
committed
checkpoint
markusdemedeiros
committed
checkpoint
markusdemedeiros
committed
checkpoint
markusdemedeiros
committed
checkpoint
markusdemedeiros
committed
solve all sorrys
markusdemedeiros
committed
checkpoint: View OFE
markusdemedeiros
committed
checkpoint: need to rebase on top of local_update PR
markusdemedeiros
committed
checkpoint: view op and pcore def
markusdemedeiros
committed
feat: view CMRA
markusdemedeiros
committed
feat: view UCMRA
markusdemedeiros
committed
op lemmas
markusdemedeiros
committed
sorry out View lemmas
markusdemedeiros
committed
Add to view
markusdemedeiros
committed
More View lemmas
markusdemedeiros
committed
sorry out breaking changes
markusdemedeiros
committed
feat: view CMRA
markusdemedeiros
committed
fix build
markusdemedeiros
committed
fix build
markusdemedeiros
committed
fix
markusdemedeiros
committed
sorry-free
markusdemedeiros
committed

Commits on Jul 9, 2025

Commits on Jul 18, 2025

fix bogus definition
markusdemedeiros
committed

Commits on Jul 19, 2025

Commits on Jul 29, 2025

Commits on Sep 4, 2025

some refactoring on agree
markusdemedeiros
committed