aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* delete backup fileHEADmasterMarcos Magueta2026-07-231-29/+0
|
* add gplv3Marcos Magueta2026-07-131-0/+674
|
* repl output drops uninformative self bindingsMarcos Magueta2026-07-121-1/+9
|
* repl session commands: load, reset, quit; emacs load-file bindingMarcos Magueta2026-07-124-27/+101
|
* lsp gains hover, definition and completion from a text-level symbol scanMarcos Magueta2026-07-124-28/+364
|
* language server over stdio, emacs mode with repl and eglot wiringMarcos Magueta2026-07-1212-12/+589
|
* package build carries menhir and rocq, docs completeness passMarcos Magueta2026-07-124-1/+25
|
* relation references as a term kind, written #NameMarcos Magueta2026-07-1215-18/+156
|
* interval characterization proofs and worked examplesMarcos Magueta2026-07-1210-2/+323
|
* branch world: state scoped reads, insert transitions, tip commitMarcos Magueta2026-07-1210-18/+523
|
* lexicographic order proven well founded, checker extracted and verifying ↵Marcos Magueta2026-07-129-4/+157
| | | | admission
* algebraic identities of plus and times discharge symbolicallyMarcos Magueta2026-07-124-12/+79
|
* decision 14: no application in term position, spec example rewritten flatMarcos Magueta2026-07-123-4/+58
|
* symbolic discharge: universals over infinite domains decided by intervalsMarcos Magueta2026-07-126-25/+313
|
* interval propagation: contradictions fail, finite ranges enumerateMarcos Magueta2026-07-114-21/+242
|
* 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 17:49:46 +0000