summaryrefslogtreecommitdiff
path: root/source/Test/Unit
AgeCommit message (Collapse)Author
2026-07-23Make `Contradiction` a proof-terminal keywordadelon
2026-07-23Use semantic subset formula inside inductive defnsadelon
2026-07-03Track ownership of top-level symbolsadelon
Require every ownable top-level symbol to be introduced by a dedicated owner before it can appear in facts. Reject duplicate ownership and prevent symbols used by inductive definitions from being defined later. Use the ownership/dependency information to reject hidden recursive inductive definitions and to generate referenceable inductive principles. BREAKING CHANGE: Top-level facts no longer introduce symbols implicitly.
2026-04-14Prefix URLs with directory (e.g. `library/`)adelon
2026-04-13Render derived facts for datatypesadelon
2026-04-13Reserve internal labels generated by datatypesadelon
2026-04-13Implement datatypesadelon
2026-04-12Update relevance filteradelon
2026-04-12Refine handling of struct labelsadelon
2026-04-12Make handling of local variables stricteradelon
2026-04-12Make lexer more robustadelon
2026-04-11Add links to tooltipadelon
2026-04-11Pin tooltip (WIP)adelon
2026-04-11Consolidate reference avalanchesadelon
2026-04-11Cross-link theoriesadelon
2026-04-11Make tooltips more efficient (less markup)adelon
2026-04-11Add brute force tooltipsadelon
2026-02-24Put failed TPTP to stderr in all cases againadelon
2026-02-24Skip intermediate datatypeadelon
2026-02-24Parse Vampire answersadelon
2026-02-24Sketch parser for Vampire's status linesadelon
2026-02-12Delete Nominal.hsadelon
2026-02-11Nominal sketchadelon
2026-02-06Make `DeBruijn.substitute` match formalizationadelon
2026-02-05Cache hypothesis lineadelon
2026-02-05Cache encoding of hypothesesadelon
2026-02-05Remove `lookupLexicalItem`, attach info in AST insteadadelon
2026-02-05Remove `lookupOp` and add marker to AST insteadadelon
2025-12-14Add location info to conjectureadelon
Still some `<nowhere>` value as placeholder left over.
2025-12-13Start inlining more testsadelon
2025-12-12Update `ReplExpr` definitionsadelon
2025-12-11More on indexed variablesadelon
2025-12-09Propagate location info furtheradelon
2025-12-04Sketch out exprs with scoped de Bruijn indicesadelon
2024-02-10Initial commitadelon
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 23:51:05 +0000