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