summaryrefslogtreecommitdiff
path: root/source
AgeCommit message (Collapse)Author
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 daysExport lexer guard through Baseadelon
11 daysMake `Omitted` carry its locationadelon
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-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-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-11Add links to tooltipadelon
2026-04-11Pin tooltip (WIP)adelon
2026-04-11Consolidate reference avalanchesadelon
2026-04-11Update Html.hsadelon
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-08Align rendering closer to sourceadelon
2026-03-07Render symbolic definitions with `=`adelon
2026-03-07Optimize HTMLadelon
2026-03-07Slightly optimize HTMLadelon
2026-03-07Use shorter custom elements in HTML markupadelon
2026-03-07Slightly optimize HTMLadelon
2026-03-07Slightly less verbose MathML renderingadelon
2026-03-07Style reference linksadelon
2026-03-07Add TOC searchadelon
2026-03-07Fix spacing in finite set expressionsadelon
2026-03-07Improve HTML rendering of comprehensionsadelon
2026-03-07Preserve marker for prefix predicatesadelon
2026-03-07Make ticked variables italicadelon
2026-03-07Improve variable renderingadelon
2026-03-07Fix rendering warningadelon
2026-03-07Fix TOC highlighting upon clicking TOC entryadelon
2026-03-07Add TOC synced highlighting (slightly janky still)adelon
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 21:28:51 +0000