summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
10 daysRequire complete Vampire success classificationadelon
10 daysReject unsound disjunctive `Assume` reductionadelon
10 daysExpose resolved workspace parsingadelon
10 daysRename Haskell package to felixadelon
10 daysReturn malformed lexical scans as typed errorsadelon
10 daysReport lexical collisions with source locationsadelon
Built-in patterns remain authoritative syntax seeds: their first source declaration records provenance without replacing the seeded marker.
10 daysParse the resolved physical source graphadelon
10 daysLoad selected sources as strict UTF-8adelon
11 daysDefine mounted source identity policyadelon
11 daysRetire unsound proof cacheadelon
11 daysSeparate golden acceptance from testsadelon
11 daysExport lexer guard through Baseadelon
11 daysMake `Omitted` carry its locationadelon
11 daysUpdate package.yamladelon
11 daysUpdate Unit.hsadelon
11 daysSimplifyadelon
14 daysPrevent self-referential definitionsadelon
14 daysReject Object-Symbol Marker Collisionsadelon
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-30Update munkres.dkgfadelon
2026-04-30Update munkres0.dkgfadelon
2026-04-30Update munkres0.dkgfadelon
2026-04-30Create munkres0.dkgfadelon
2026-04-30Create munkres.dkgfadelon
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-13Add basic website deploymentadelon
2026-04-12Update relevance filteradelon
2026-04-12Handle bounded calculationsadelon
2026-04-12Refine handling of struct labelsadelon
2026-04-12Make handling of local variables stricteradelon
2026-04-12Make lexer more robustadelon
2026-04-12Update lexicon.tsvadelon
2026-04-11Add links to tooltipadelon
2026-04-11Pin tooltip (WIP)adelon
2026-04-11Consolidate reference avalanchesadelon
2026-04-11Create Caddyfileadelon
2026-04-11Update Html.hsadelon
2026-04-11Update lexicon.tsvadelon
2026-04-11Cross-link theoriesadelon
2026-04-11Make tooltips more efficient (less markup)adelon
2026-04-11Add brute force tooltipsadelon
2026-03-25Update temporary warnings for easier debuggingadelon
2026-03-25Update parsing.goldenadelon
2026-03-20Update .gitignoreadelon
2026-03-08Align rendering closer to sourceadelon
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 19:57:28 +0000