aboutsummaryrefslogtreecommitdiffstats
path: root/theories/dune (follow)
Commit message (Collapse)AuthorAgeFilesLines
* interval characterization proofs and worked examplesMarcos Magueta2026-07-121-1/+8
|
* lexicographic order proven well founded, checker extracted and verifying ↵Marcos Magueta2026-07-121-1/+8
| | | | admission
* admission runs the containment checker extracted from rocqMarcos Magueta2026-07-111-3/+10
|
* rocq proof: structural decrease is well foundedMarcos Magueta2026-07-111-0/+13