aboutsummaryrefslogtreecommitdiffstats
path: root/test/test_vm.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* algebraic identities of plus and times discharge symbolicallyMarcos Magueta2026-07-121-0/+16
|
* symbolic discharge: universals over infinite domains decided by intervalsMarcos Magueta2026-07-121-5/+49
|
* interval propagation: contradictions fail, finite ranges enumerateMarcos Magueta2026-07-111-0/+32
|
* mutual recursion admitted under lexicographic measuresMarcos Magueta2026-07-111-4/+44
|
* world relation as the universe for scoped negationMarcos Magueta2026-07-111-0/+8
|
* residuation: open membership returns residual constraintsMarcos Magueta2026-07-111-8/+35
|
* admission runs the containment checker extracted from rocqMarcos Magueta2026-07-111-0/+15
|
* embedding surface, host world test, deep recursion, line trackingMarcos Magueta2026-07-111-0/+11
|
* negation, quantifiers and membership criteria as schema domainsMarcos Magueta2026-07-111-3/+131
|
* working vm: parser, admission with totality checks, solver and replMarcos Magueta2026-07-111-0/+200
generated by cgit v1.2.3 (git 2.25.1) at 2026-11-04 01:52:05 +0000