aboutsummaryrefslogtreecommitdiffstats
path: root/lib (follow)
Commit message (Collapse)AuthorAgeFilesLines
* branch world: state scoped reads, insert transitions, tip commitMarcos Magueta2026-07-125-9/+291
|
* lexicographic order proven well founded, checker extracted and verifying ↵Marcos Magueta2026-07-124-3/+36
| | | | admission
* algebraic identities of plus and times discharge symbolicallyMarcos Magueta2026-07-121-2/+49
|
* symbolic discharge: universals over infinite domains decided by intervalsMarcos Magueta2026-07-121-6/+233
|
* interval propagation: contradictions fail, finite ranges enumerateMarcos Magueta2026-07-111-10/+185
|
* mutual recursion admitted under lexicographic measuresMarcos Magueta2026-07-113-75/+159
|
* world relation as the universe for scoped negationMarcos Magueta2026-07-111-0/+4
|
* residuation: open membership returns residual constraintsMarcos Magueta2026-07-113-44/+138
|
* admission runs the containment checker extracted from rocqMarcos Magueta2026-07-113-6/+52
|
* embedding surface, host world test, deep recursion, line trackingMarcos Magueta2026-07-112-1/+9
|
* negation, quantifiers and membership criteria as schema domainsMarcos Magueta2026-07-118-74/+342
|
* working vm: parser, admission with totality checks, solver and replMarcos Magueta2026-07-1114-0/+1259
|
* canonical term algebra: labels, records, rationals, sequencesMarcos Magueta2026-07-115-0/+228