summaryrefslogtreecommitdiff
path: root/source/Render/Html.hs
AgeCommit message (Collapse)Author
3 hoursMigrate to `Felix` namespaceHEADhotgadelon
3 daysTighten sequential HTML presentation ownershipadelon
3 daysShare HTML target and route analysisadelon
3 daysReuse verified presentation for HTMLadelon
10 daysRoute HTML links through render contextadelon
10 daysSuppress unchecked datatype fact previewsadelon
HTML currently has only raw datatype syntax, while checked facts may use canonical domains. Omit derived facts until checked semantic context reaches the renderer.
10 daysConfine HTML export writesadelon
11 daysExport lexer guard through Baseadelon
11 daysMake `Omitted` carry its locationadelon
14 daysMake `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-13Implement datatypesadelon
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-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
2026-03-07Make references linksadelon
2026-03-07Update Html.hsadelon
2026-03-07Deduplicate warnings for missing render hintsadelon
2026-03-07Refine TOCadelon
2026-03-07Update TOCadelon
2026-03-07Add basic dark mode support in HTML rendereradelon
2026-03-07Render markeradelon
2026-03-07Simplify HTML renderingadelon
2026-03-07Fix rendering of relation symbolsadelon
2026-03-07Add HTML rendering skeletonadelon
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 19:09:35 +0000