aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* mutual recursion admitted under lexicographic measuresMarcos Magueta2026-07-117-97/+228
* world relation as the universe for scoped negationMarcos Magueta2026-07-112-0/+12
* residuation: open membership returns residual constraintsMarcos Magueta2026-07-118-76/+223
* admission runs the containment checker extracted from rocqMarcos Magueta2026-07-118-12/+253
* virtual machine specification documentMarcos Magueta2026-07-112-8/+140
* rocq proof: structural decrease is well foundedMarcos Magueta2026-07-119-2/+80
* core design and pipeline documentMarcos Magueta2026-07-112-10/+142
* embedding surface, host world test, deep recursion, line trackingMarcos Magueta2026-07-117-6/+136
* negation, quantifiers and membership criteria as schema domainsMarcos Magueta2026-07-1111-79/+510
* working vm: parser, admission with totality checks, solver and replMarcos Magueta2026-07-1121-2/+1631
* lock nixpkgs and generated opam metadataMarcos Magueta2026-07-111-0/+27
* canonical term algebra: labels, records, rationals, sequencesMarcos Magueta2026-07-118-0/+405
* nix flake with dune and rocq development environmentMarcos Magueta2026-07-114-0/+121
* 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
* readme ported from test projectMarcos Magueta2026-07-111-0/+176
generated by cgit v1.2.3 (git 2.25.1) at 2026-11-04 05:42:57 +0000