aboutsummaryrefslogtreecommitdiffstats
path: root/docs (unfollow)
Commit message (Expand)AuthorFilesLines
2026-07-12relation references as a term kind, written #NameMarcos Magueta3-4/+79
2026-07-12branch world: state scoped reads, insert transitions, tip commitMarcos Magueta2-7/+77
2026-07-12algebraic identities of plus and times discharge symbolicallyMarcos Magueta2-10/+14
2026-07-12decision 14: no application in term position, spec example rewritten flatMarcos Magueta2-3/+54
2026-07-12symbolic discharge: universals over infinite domains decided by intervalsMarcos Magueta3-13/+27
2026-07-11interval propagation: contradictions fail, finite ranges enumerateMarcos Magueta2-11/+25
2026-07-11mutual recursion admitted under lexicographic measuresMarcos Magueta3-18/+25
2026-07-11residuation: open membership returns residual constraintsMarcos Magueta2-10/+23
2026-07-11admission runs the containment checker extracted from rocqMarcos Magueta2-3/+58
2026-07-11virtual machine specification documentMarcos Magueta1-0/+131
2026-07-11core design and pipeline documentMarcos Magueta1-0/+129
2026-07-11embedding surface, host world test, deep recursion, line trackingMarcos Magueta1-0/+10
2026-07-11negation, quantifiers and membership criteria as schema domainsMarcos Magueta1-0/+35
2026-07-11working vm: parser, admission with totality checks, solver and replMarcos Magueta1-0/+83
2026-07-11canonical term algebra: labels, records, rationals, sequencesMarcos Magueta1-0/+48
2026-07-11implementation language decision: ocaml with rocq extractionMarcos Magueta1-0/+26
2026-07-11sakura + RNT integration document with decisions from planningMarcos Magueta1-0/+722
2026-07-11language specification documentMarcos Magueta1-0/+1336