aboutsummaryrefslogtreecommitdiffstats
path: root/docs (follow)
Commit message (Collapse)AuthorAgeFilesLines
* algebraic identities of plus and times discharge symbolicallyMarcos Magueta2026-07-122-10/+14
|
* decision 14: no application in term position, spec example rewritten flatMarcos Magueta2026-07-122-3/+54
|
* symbolic discharge: universals over infinite domains decided by intervalsMarcos Magueta2026-07-123-13/+27
|
* interval propagation: contradictions fail, finite ranges enumerateMarcos Magueta2026-07-112-11/+25
|
* mutual recursion admitted under lexicographic measuresMarcos Magueta2026-07-113-18/+25
|
* residuation: open membership returns residual constraintsMarcos Magueta2026-07-112-10/+23
|
* admission runs the containment checker extracted from rocqMarcos Magueta2026-07-112-3/+58
|
* virtual machine specification documentMarcos Magueta2026-07-111-0/+131
|
* core design and pipeline documentMarcos Magueta2026-07-111-0/+129
|
* embedding surface, host world test, deep recursion, line trackingMarcos Magueta2026-07-111-0/+10
|
* negation, quantifiers and membership criteria as schema domainsMarcos Magueta2026-07-111-0/+35
|
* working vm: parser, admission with totality checks, solver and replMarcos Magueta2026-07-111-0/+83
|
* canonical term algebra: labels, records, rationals, sequencesMarcos Magueta2026-07-111-0/+48
|
* implementation language decision: ocaml with rocq extractionMarcos Magueta2026-07-111-0/+26
|
* sakura + RNT integration document with decisions from planningMarcos Magueta2026-07-111-0/+722
|
* language specification documentMarcos Magueta2026-07-111-0/+1336
generated by cgit v1.2.3 (git 2.25.1) at 2026-11-04 08:59:28 +0000