Migrate to `Felix` namespaceHEADhotg

1 files changed, 3964 insertions, 0 deletions

diff --git a/source/Felix/Render/Html.hs b/source/Felix/Render/Html.hs
new file mode 100644
index 0000000..7081e52
--- /dev/null
+++ b/source/Felix/Render/Html.hs
@@ -0,0 +1,3964 @@
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+
+module Felix.Render.Html
+    ( HtmlRenderIndex
+    , HtmlPagePresentation
+    , buildRenderIndex
+    , htmlPagePresentationSource
+    , renderDocument
+    , supportScriptAssetContents
+    ) where
+
+import Felix.Syntax.Abstract
+
+import Base
+import Felix.Source (ResolvedSource)
+import Lucid hiding (Term, for_)
+import Lucid.Base (makeAttributes)
+import Lucid.Math
+import Felix.Render.Html.Context
+    ( HtmlRenderContext
+    , HtmlRenderContextError
+    , htmlCurrentPageLabel
+    , htmlCurrentSource
+    , htmlSourceFragmentHref
+    , htmlSourceLabel
+    , htmlSourcePageHref
+    , htmlSupportScriptHref
+    )
+import Felix.Render.Html.Layout (renderUrlFragment)
+import Felix.Report.Location (Location, pattern Nowhere)
+import Felix.Syntax.Token (VariableDisplay(..), VariableSuffix(..), displayVariable, tokToText)
+
+import Control.Monad (unless, when)
+import Data.Char (digitToInt, isAlphaNum, isDigit, isSpace, toUpper)
+import Data.List qualified as List
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Map.Strict qualified as Map
+import Data.Set qualified as Set
+import Data.Text qualified as Text
+import Data.Text.Lazy qualified as LazyText
+
+
+
+data HintCategory
+    = OperatorHint
+    | RelationHint
+    | PredicateHint
+    | StructOpHint
+    deriving (Show, Eq, Ord)
+
+data TemplatePiece
+    = Literal Text
+    | Slot Int
+    deriving (Show, Eq, Ord)
+
+data RenderHint = RenderHint
+    { renderHintArity :: Int
+    , renderHintTemplate :: [TemplatePiece]
+    } deriving (Show, Eq, Ord)
+
+type HintMap = Map (HintCategory, Marker, Int) RenderHint
+type AnchorMap = Map Marker Text
+type BlockRenderInfo = (Int, Block, Text)
+type PreviewMap = Map Marker PreviewEntry
+
+data HtmlRenderIndex = HtmlRenderIndex
+    !(Map Marker IndexedReferenceTarget)
+
+data HtmlPagePresentation = HtmlPagePresentation
+    { htmlPagePresentationSource :: !ResolvedSource
+    , pagePresentationBlockInfos :: ![BlockRenderInfo]
+    , pagePresentationAnchors :: !AnchorMap
+    , pagePresentationReferencedMarkers :: !(Set Marker)
+    }
+
+data IndexedReferenceTarget = IndexedReferenceTarget
+    !Int
+    !ResolvedSource
+    !ReferenceTarget
+
+data ReferenceContext = ReferenceContext
+    { referenceAnchors :: AnchorMap
+    , referencePreviews :: PreviewMap
+    }
+
+data PreviewEntry = PreviewEntry
+    { previewMarker :: Marker
+    , previewKind :: Text
+    , previewTitle :: Maybe Text
+    , previewSourceLabel :: Text
+    , previewSourceHref :: Text
+    , previewReferenceHref :: Text
+    , previewId :: Text
+    , previewBody :: HintMap -> Html ()
+    }
+
+data ReferenceTarget = ReferenceTarget
+    { targetMarker :: Marker
+    , targetAnchorId :: Text
+    , targetKind :: Text
+    , targetTitle :: Maybe Text
+    , targetBody :: HintMap -> Html ()
+    }
+
+data StmtMathFragment
+    = StmtMathProse Text
+    | StmtMathNode (Html ())
+
+type StmtMathFragments = [StmtMathFragment]
+
+newtype MissingHintMap = MissingHintMap
+    { unMissingHintMap :: Map HintCategory (Set Marker)
+    } deriving (Show, Eq)
+
+instance Semigroup MissingHintMap where
+    MissingHintMap left <> MissingHintMap right =
+        MissingHintMap (Map.unionWith (<>) left right)
+
+instance Monoid MissingHintMap where
+    mempty = MissingHintMap mempty
+
+proofCollapseThreshold :: Int
+proofCollapseThreshold = 10
+
+referenceGroupThreshold :: Int
+referenceGroupThreshold = 5
+
+
+renderDocument
+    :: HtmlRenderContext
+    -> Text
+    -> HtmlRenderIndex
+    -> HtmlPagePresentation
+    -> Either HtmlRenderContextError Text
+renderDocument
+        context
+        hintsSource
+        renderIndex
+        HtmlPagePresentation
+            { pagePresentationBlockInfos = blockInfos
+            , pagePresentationAnchors = anchors
+            , pagePresentationReferencedMarkers = referencedMarkers
+            } = do
+    previews <-
+        buildPreviewMap
+            context
+            referencedMarkers
+            anchors
+            renderIndex
+    let result =
+            case formatMissingHintWarning missingHints of
+                Nothing -> rendered
+                Just warningText ->
+                    trace (Text.unpack warningText) rendered
+        hints = parseHints hintsSource
+        missingHints =
+            collectMissingHints
+                hints
+                [ block
+                | (_index, block, _blockId) <- blockInfos
+                ]
+        rendered = LazyText.toStrict (renderText (renderPage hints))
+        pageLabel = htmlCurrentPageLabel context
+        tocBlocks = [(index, blockId, block) | (index, block, blockId) <- blockInfos, includeInToc block]
+        referenceContext = ReferenceContext anchors previews
+
+        renderPage :: HintMap -> Html ()
+        renderPage hintMap = doctypehtml_ do
+            head_ do
+                meta_ [charset_ "utf-8"]
+                title_ (toHtml pageLabel)
+                style_ pageStyles
+            body_ do
+                div_ [class_ "page-layout"] do
+                    aside_ [class_ "toc-column"] do
+                        nav_ [class_ "toc"] do
+                            h2_ [class_ "toc-heading"] "Contents"
+                            input_
+                                [ class_ "toc-filter"
+                                , type_ "search"
+                                , placeholder_ "Filter labels"
+                                , makeAttributes "aria-label" "Filter TOC by label"
+                                ]
+                            ol_ [class_ "toc-list"] do
+                                traverse_ renderTocEntry tocBlocks
+                    main_ do
+                        h1_ (toHtml pageLabel)
+                        traverse_ (renderBlock hintMap referenceContext) blockInfos
+                renderPreviewStore hintMap previews
+                div_
+                    [ id_ "reference-preview-popup"
+                    , class_ "reference-preview-popup"
+                    , makeAttributes "role" "tooltip"
+                    , makeAttributes "aria-hidden" "true"
+                    ]
+                    skip
+                script_
+                    [src_ (htmlSupportScriptHref context)]
+                    ("" :: Text)
+    Right result
+
+-- | Index every block target and every page's referenced markers once in
+-- deterministic source order.  Rendering a page subsequently performs only
+-- marker lookups in the shared index.
+buildRenderIndex
+    :: NonEmpty (ResolvedSource, [Block])
+    -> (HtmlRenderIndex, NonEmpty HtmlPagePresentation)
+buildRenderIndex sourceBlocks =
+    ( HtmlRenderIndex
+        (Map.fromList
+            [ ( targetMarker target
+              , IndexedReferenceTarget ordinal source target
+              )
+            | (ordinal, (source, target)) <-
+                zip [1 :: Int ..] orderedTargets
+            ])
+    , pages
+    )
+  where
+    analysedPages =
+        uncurry analysePage <$> sourceBlocks
+    pages =
+        fst <$> analysedPages
+    orderedTargets =
+        [ (htmlPagePresentationSource page, target)
+        | (page, targets) <- NonEmpty.toList analysedPages
+        , target <- targets
+        ]
+
+    analysePage source blocks =
+        ( HtmlPagePresentation
+            { htmlPagePresentationSource = source
+            , pagePresentationBlockInfos = blockInfos
+            , pagePresentationAnchors =
+                Map.fromList
+                    [ (targetMarker, targetAnchorId)
+                    | ReferenceTarget
+                        { targetMarker
+                        , targetAnchorId
+                        } <- targets
+                    ]
+            , pagePresentationReferencedMarkers =
+                foldMap
+                    (\(_blockInfo, _targets, references) -> references)
+                    analysedBlocks
+            }
+        , targets
+        )
+      where
+        analysedBlocks =
+            [ ( blockInfo
+              , referenceTargetsOfBlockRenderInfo blockInfo
+              , collectReferencedMarkersOfBlock block
+              )
+            | (index, block) <- zip [1 :: Int ..] blocks
+            , let blockInfo =
+                    (index, block, blockAnchorId index block)
+            ]
+        blockInfos =
+            [ blockInfo
+            | (blockInfo, _targets, _references) <- analysedBlocks
+            ]
+        targets =
+            concat
+                [ blockTargets
+                | (_blockInfo, blockTargets, _references) <- analysedBlocks
+                ]
+
+
+pageStyles :: Text
+pageStyles = Text.unlines
+    [ ":root {"
+    , "  color-scheme: light dark;"
+    , "  font-family: Georgia, \"Times New Roman\", serif;"
+    , "  --page-bg: #ffffff;"
+    , "  --page-fg: #111111;"
+    , "  --muted-fg: #666666;"
+    , "  --subtle-fg: #444444;"
+    , "  --badge-bg: #f1f1f1;"
+    , "  --badge-border: #dddddd;"
+    , "  --badge-fg: #555555;"
+    , "  --rule-color: #d9d2c2;"
+    , "  --error-fg: #9f1d1d;"
+    , "  --error-bg: #fff1f1;"
+    , "  --toc-active-bg: #f3efe6;"
+    , "  --toc-active-fg: #1b1b1b;"
+    , "  --toc-active-accent: #b9aa7a;"
+    , "  --preview-bg: #fffdf8;"
+    , "  --preview-border: #cfc3a3;"
+    , "  --preview-shadow: rgba(0, 0, 0, 0.18);"
+    , "}"
+    , "html {"
+    , "  height: 100%;"
+    , "}"
+    , "body {"
+    , "  margin: 0;"
+    , "  height: 100vh;"
+    , "  overflow: hidden;"
+    , "  line-height: 1.5;"
+    , "  background: var(--page-bg);"
+    , "  color: var(--page-fg);"
+    , "}"
+    , ".page-layout {"
+    , "  display: grid;"
+    , "  grid-template-columns: minmax(16rem, 24rem) minmax(0, 1fr);"
+    , "  grid-template-rows: minmax(0, 1fr);"
+    , "  gap: 2rem;"
+    , "  align-items: stretch;"
+    , "  box-sizing: border-box;"
+    , "  margin: 0 auto;"
+    , "  max-width: 84rem;"
+    , "  height: 100vh;"
+    , "  padding: 2rem 1.25rem 3rem;"
+    , "}"
+    , ".toc-column {"
+    , "  display: block;"
+    , "  min-height: 0;"
+    , "}"
+    , ".toc {"
+    , "  display: flex;"
+    , "  flex-direction: column;"
+    , "  height: 100%;"
+    , "  min-height: 0;"
+    , "}"
+    , ".toc-heading {"
+    , "  margin: 0 0 0.75rem;"
+    , "  color: var(--muted-fg);"
+    , "  font-size: 0.9rem;"
+    , "  letter-spacing: 0.04em;"
+    , "  text-transform: uppercase;"
+    , "}"
+    , ".toc-filter {"
+    , "  box-sizing: border-box;"
+    , "  width: 100%;"
+    , "  margin: 0 0 0.9rem;"
+    , "  padding: 0.45rem 0.55rem;"
+    , "  border: 1px solid var(--badge-border);"
+    , "  border-radius: 0.35rem;"
+    , "  background: var(--page-bg);"
+    , "  color: var(--page-fg);"
+    , "  font: inherit;"
+    , "}"
+    , ".toc-filter::placeholder {"
+    , "  color: var(--muted-fg);"
+    , "}"
+    , ".toc-list {"
+    , "  flex: 1 1 auto;"
+    , "  min-height: 0;"
+    , "  overflow-y: auto;"
+    , "  list-style: none;"
+    , "  margin: 0;"
+    , "  padding: 0 0.5rem 0 0;"
+    , "}"
+    , ".toc-list > li {"
+    , "  margin: 0 0 0.8rem;"
+    , "}"
+    , ".toc-list > li > a {"
+    , "  display: block;"
+    , "  margin: -0.15rem -0.35rem;"
+    , "  padding: 0.15rem 0.35rem;"
+    , "  border-radius: 0.35rem;"
+    , "  color: inherit;"
+    , "  text-decoration: none;"
+    , "  transition: background-color 120ms ease, box-shadow 120ms ease, color 120ms ease;"
+    , "}"
+    , ".toc-list > li > a:hover,"
+    , ".toc-list > li > a:focus-visible {"
+    , "  text-decoration: underline;"
+    , "}"
+    , ".toc-list > li > a.is-active {"
+    , "  background: var(--toc-active-bg);"
+    , "  box-shadow: inset 0.2rem 0 0 var(--toc-active-accent);"
+    , "  color: var(--toc-active-fg);"
+    , "}"
+    , ".toc-list > li > a.is-active > code {"
+    , "  color: var(--toc-active-fg);"
+    , "}"
+    , ".toc-list > li > a > span:first-child {"
+    , "  display: block;"
+    , "  font-weight: 700;"
+    , "}"
+    , ".toc-list > li > a > code {"
+    , "  display: block;"
+    , "  margin-top: 0.15rem;"
+    , "  color: var(--muted-fg);"
+    , "  font-size: 0.9em;"
+    , "  overflow-wrap: anywhere;"
+    , "}"
+    , "main {"
+    , "  min-width: 0;"
+    , "  min-height: 0;"
+    , "  overflow-y: auto;"
+    , "}"
+    , "main > *[id] {"
+    , "  display: block;"
+    , "  margin: 0 0 1rem;"
+    , "  scroll-margin-top: 1rem;"
+    , "}"
+    , "head- {"
+    , "  font-weight: 700;"
+    , "}"
+    , "title- {"
+    , "  font-weight: 400;"
+    , "}"
+    , "id-,"
+    , "main a[href^=\"#\"],"
+    , ".ref-badge {"
+    , "  display: inline-block;"
+    , "  padding: 0.02rem 0.35rem;"
+    , "  border: 1px solid var(--badge-border);"
+    , "  border-radius: 0.2rem;"
+    , "  background: var(--badge-bg);"
+    , "  color: var(--badge-fg);"
+    , "  font-family: \"SFMono-Regular\", Menlo, Consolas, \"Liberation Mono\", monospace;"
+    , "  font-size: 0.82em;"
+    , "  text-decoration: none;"
+    , "}"
+    , "head- > id- {"
+    , "  margin-left: 0.45rem;"
+    , "}"
+    , "main a[href^=\"#\"]:hover,"
+    , "main a[href^=\"#\"]:focus-visible,"
+    , ".ref-badge.has-preview:hover,"
+    , ".ref-badge.has-preview:focus-visible {"
+    , "  text-decoration: underline;"
+    , "}"
+    , ".ref-badge.has-preview {"
+    , "  cursor: help;"
+    , "}"
+    , ".ref-badge-group {"
+    , "  user-select: none;"
+    , "}"
+    , "proof- > p:first-child,"
+    , "proof- > details > summary + p {"
+    , "  display: inline;"
+    , "  margin: 0;"
+    , "}"
+    , "proof- proof- {"
+    , "  display: block;"
+    , "  margin: 0.5rem 0 0.5rem 1rem;"
+    , "  padding-left: 0.75rem;"
+    , "  border-left: 1px solid var(--rule-color);"
+    , "}"
+    , "proof- > details {"
+    , "  margin: 0;"
+    , "}"
+    , "proof- > details > summary {"
+    , "  cursor: pointer;"
+    , "  font-weight: 700;"
+    , "}"
+    , "proof- > details > summary title- {"
+    , "  font-weight: 400;"
+    , "}"
+    , "proof- > details > :not(summary) {"
+    , "  margin-top: 0.5rem;"
+    , "}"
+    , "inductive- > details {"
+    , "  margin-top: 0.75rem;"
+    , "}"
+    , "inductive- > details > summary {"
+    , "  cursor: pointer;"
+    , "  font-weight: 700;"
+    , "}"
+    , "inductive- > details > :not(summary) {"
+    , "  margin-top: 0.5rem;"
+    , "}"
+    , ".inductive-derived-facts > li {"
+    , "  margin: 0.35rem 0;"
+    , "}"
+    , ".inductive-derived-facts {"
+    , "  margin: 0;"
+    , "  padding-left: 1.5rem;"
+    , "}"
+    , ".reference-preview-store {"
+    , "  display: none;"
+    , "}"
+    , ".reference-preview-popup {"
+    , "  position: fixed;"
+    , "  z-index: 1000;"
+    , "  box-sizing: border-box;"
+    , "  width: 44rem;"
+    , "  max-width: calc(100vw - 2rem);"
+    , "  max-height: 34rem;"
+    , "  max-height: min(34rem, calc(100vh - 2rem));"
+    , "  overflow: auto;"
+    , "  overscroll-behavior: contain;"
+    , "  padding: 0.75rem 0.9rem;"
+    , "  border: 1px solid var(--preview-border);"
+    , "  border-radius: 0.45rem;"
+    , "  background: var(--preview-bg);"
+    , "  color: var(--page-fg);"
+    , "  box-shadow: 0 0.75rem 2.25rem var(--preview-shadow);"
+    , "  opacity: 0;"
+    , "  pointer-events: none;"
+    , "  transform: translateY(0.2rem);"
+    , "  transition: opacity 90ms ease, transform 90ms ease;"
+    , "}"
+    , ".reference-preview-popup[aria-hidden=\"true\"] {"
+    , "  visibility: hidden;"
+    , "}"
+    , ".reference-preview-popup.is-visible {"
+    , "  opacity: 1;"
+    , "  pointer-events: auto;"
+    , "  transform: translateY(0);"
+    , "}"
+    , ".reference-preview-popup * {"
+    , "  box-sizing: border-box;"
+    , "}"
+    , ".reference-preview-template {"
+    , "  display: flex;"
+    , "  flex-direction: column;"
+    , "  gap: 0.45rem;"
+    , "  width: 100%;"
+    , "}"
+    , ".reference-preview-heading {"
+    , "  display: block;"
+    , "  margin: 0;"
+    , "  width: 100%;"
+    , "  color: var(--muted-fg);"
+    , "  font-size: 0.82rem;"
+    , "  letter-spacing: 0.035em;"
+    , "  text-transform: uppercase;"
+    , "}"
+    , ".reference-preview-heading code {"
+    , "  color: var(--page-fg);"
+    , "  font-family: \"SFMono-Regular\", Menlo, Consolas, \"Liberation Mono\", monospace;"
+    , "  letter-spacing: 0;"
+    , "  text-transform: none;"
+    , "}"
+    , ".reference-preview-heading a {"
+    , "  color: inherit;"
+    , "  text-decoration: none;"
+    , "}"
+    , ".reference-preview-heading a:hover,"
+    , ".reference-preview-heading a:focus-visible {"
+    , "  text-decoration: underline;"
+    , "}"
+    , ".reference-preview-source {"
+    , "  display: block;"
+    , "  margin: 0;"
+    , "  color: var(--subtle-fg);"
+    , "  font-size: 0.78rem;"
+    , "  letter-spacing: 0;"
+    , "  text-transform: none;"
+    , "}"
+    , ".reference-preview-body {"
+    , "  display: block;"
+    , "  clear: both;"
+    , "  margin: 0;"
+    , "  width: 100%;"
+    , "}"
+    , ".reference-preview-body p {"
+    , "  margin: 0.35rem 0 0;"
+    , "}"
+    , ".reference-preview-body p:first-child {"
+    , "  margin-top: 0;"
+    , "}"
+    , ".reference-preview-group-template {"
+    , "  display: flex;"
+    , "  flex-direction: column;"
+    , "  gap: 1rem;"
+    , "  margin: 0;"
+    , "  width: 100%;"
+    , "}"
+    , ".reference-preview-group-template > .reference-preview-template + .reference-preview-template {"
+    , "  padding-top: 1rem;"
+    , "  border-top: 1px solid var(--badge-border);"
+    , "}"
+    , ".reference-preview-statement {"
+    , "  display: block;"
+    , "  width: 100%;"
+    , "  white-space: normal;"
+    , "  overflow-wrap: break-word;"
+    , "}"
+    , ".reference-preview-statement math {"
+    , "  max-width: 100%;"
+    , "  overflow-x: auto;"
+    , "  overflow-y: hidden;"
+    , "  vertical-align: middle;"
+    , "}"
+    , "math[display=\"block\"] {"
+    , "  display: block;"
+    , "  margin: 0.5rem 0;"
+    , "}"
+    , "merror {"
+    , "  color: var(--error-fg);"
+    , "  background: var(--error-bg);"
+    , "}"
+    , "@media (prefers-color-scheme: dark) {"
+    , "  :root {"
+    , "    --page-bg: #161616;"
+    , "    --page-fg: #e9e6df;"
+    , "    --muted-fg: #b7b0a4;"
+    , "    --subtle-fg: #cfc8bc;"
+    , "    --badge-bg: #2a2a2a;"
+    , "    --badge-border: #444444;"
+    , "    --badge-fg: #d8d3ca;"
+    , "    --rule-color: #5b5348;"
+    , "    --error-fg: #ffb0b0;"
+    , "    --error-bg: #3b1f1f;"
+    , "    --toc-active-bg: #2b271f;"
+    , "    --toc-active-fg: #f0ebe1;"
+    , "    --toc-active-accent: #99865a;"
+    , "    --preview-bg: #211f1a;"
+    , "    --preview-border: #776a50;"
+    , "    --preview-shadow: rgba(0, 0, 0, 0.55);"
+    , "  }"
+    , "}"
+    , "@media (max-width: 900px) {"
+    , "  body {"
+    , "    height: auto;"
+    , "    overflow: auto;"
+    , "  }"
+    , "  .page-layout {"
+    , "    grid-template-columns: 1fr;"
+    , "    grid-template-rows: auto;"
+    , "    gap: 1.5rem;"
+    , "    height: auto;"
+    , "  }"
+    , "  .toc-column {"
+    , "    display: none;"
+    , "  }"
+    , "  main {"
+    , "    min-height: auto;"
+    , "    overflow: visible;"
+    , "  }"
+    , "}"
+    ]
+
+supportScriptAssetContents :: Text
+supportScriptAssetContents = tocScript <> "\n" <> referencePreviewScript
+
+
+tocScript :: Text
+tocScript = Text.unlines
+    [ "(function () {"
+    , "  const toc = document.querySelector('.toc');"
+    , "  const tocList = toc ? toc.querySelector('.toc-list') : null;"
+    , "  const filterInput = toc ? toc.querySelector('.toc-filter') : null;"
+    , "  const content = document.querySelector('main');"
+    , "  if (!toc || !tocList || !content) return;"
+    , "  const links = Array.from(tocList.querySelectorAll(':scope > li > a[href^=\"#\"]'));"
+    , "  const blocks = Array.from(content.querySelectorAll(':scope > *[id]'));"
+    , "  if (!links.length || !blocks.length) return;"
+    , "  const linkByTarget = new Map(links.map((link) => [decodeURIComponent(link.hash.slice(1)), link]));"
+    , "  const tocEntries = links.map((link) => ({"
+    , "    item: link.parentElement,"
+    , "    link,"
+    , "    label: ((link.querySelector('code') || link.lastElementChild || link).textContent || '').trim().toLowerCase()"
+    , "  }));"
+    , "  let activeTarget = null;"
+    , "  let rafId = 0;"
+    , "  let suspendUntil = 0;"
+    , ""
+    , "  const keepActiveLinkVisible = (link) => {"
+    , "    if (!link || performance.now() < suspendUntil) return;"
+    , "    const item = link.parentElement;"
+    , "    if (item && item.hidden) return;"
+    , "    const tocRect = tocList.getBoundingClientRect();"
+    , "    const linkRect = link.getBoundingClientRect();"
+    , "    const comfortTop = tocRect.top + tocRect.height * 0.2;"
+    , "    const comfortBottom = tocRect.bottom - tocRect.height * 0.2;"
+    , "    if (linkRect.top < comfortTop || linkRect.bottom > comfortBottom) {"
+    , "      link.scrollIntoView({ block: 'nearest', inline: 'nearest' });"
+    , "    }"
+    , "  };"
+    , ""
+    , "  const applyFilter = () => {"
+    , "    const query = filterInput ? filterInput.value.trim().toLowerCase() : '';"
+    , "    for (const { item, label } of tocEntries) {"
+    , "      if (!item) continue;"
+    , "      item.hidden = query !== '' && !label.includes(query);"
+    , "    }"
+    , "    if (activeTarget) {"
+    , "      keepActiveLinkVisible(linkByTarget.get(activeTarget));"
+    , "    }"
+    , "  };"
+    , ""
+    , "  const setActiveTarget = (target) => {"
+    , "    if (!target || target === activeTarget) return;"
+    , "    const previous = activeTarget ? linkByTarget.get(activeTarget) : null;"
+    , "    if (previous) {"
+    , "      previous.classList.remove('is-active');"
+    , "      previous.removeAttribute('aria-current');"
+    , "    }"
+    , "    activeTarget = target;"
+    , "    const next = linkByTarget.get(target);"
+    , "    if (!next) return;"
+    , "    next.classList.add('is-active');"
+    , "    next.setAttribute('aria-current', 'location');"
+    , "    keepActiveLinkVisible(next);"
+    , "  };"
+    , ""
+    , "  const firstTarget = blocks[0].id;"
+    , ""
+    , "  const findActiveTarget = () => {"
+    , "    const contentRect = content.getBoundingClientRect();"
+    , "    const topSnapThreshold = 40;"
+    , "    for (const block of blocks) {"
+    , "      const target = block.id;"
+    , "      const rect = block.getBoundingClientRect();"
+    , "      if (rect.top >= contentRect.top - 4 && rect.top <= contentRect.top + topSnapThreshold) {"
+    , "        return target;"
+    , "      }"
+    , "    }"
+    , "    const activationLine = contentRect.top + contentRect.height * 0.22;"
+    , "    let candidate = firstTarget;"
+    , "    for (const block of blocks) {"
+    , "      const target = block.id;"
+    , "      if (block.getBoundingClientRect().top <= activationLine) {"
+    , "        candidate = target;"
+    , "        continue;"
+    , "      }"
+    , "      break;"
+    , "    }"
+    , "    return candidate;"
+    , "  };"
+    , ""
+    , "  const scheduleUpdate = () => {"
+    , "    if (rafId) return;"
+    , "    rafId = window.requestAnimationFrame(() => {"
+    , "      rafId = 0;"
+    , "      setActiveTarget(findActiveTarget());"
+    , "    });"
+    , "  };"
+    , ""
+    , "  const suspendAutofollow = () => {"
+    , "    suspendUntil = performance.now() + 1500;"
+    , "  };"
+    , ""
+    , "  const revealTarget = (target) => {"
+    , "    let parent = target.parentElement;"
+    , "    while (parent) {"
+    , "      if (parent.localName === 'details') {"
+    , "        parent.open = true;"
+    , "      }"
+    , "      parent = parent.parentElement;"
+    , "    }"
+    , "  };"
+    , ""
+    , "  const scrollToTarget = (targetId) => {"
+    , "    const target = document.getElementById(targetId);"
+    , "    if (!target || !content.contains(target)) return false;"
+    , "    revealTarget(target);"
+    , "    target.scrollIntoView({ block: 'start', inline: 'nearest' });"
+    , "    setActiveTarget(targetId);"
+    , "    return true;"
+    , "  };"
+    , ""
+    , "  content.addEventListener('scroll', scheduleUpdate, { passive: true });"
+    , "  window.addEventListener('resize', scheduleUpdate);"
+    , "  tocList.addEventListener('wheel', suspendAutofollow, { passive: true });"
+    , "  tocList.addEventListener('touchstart', suspendAutofollow, { passive: true });"
+    , "  toc.addEventListener('pointerdown', suspendAutofollow);"
+    , "  toc.addEventListener('focusin', suspendAutofollow);"
+    , "  if (filterInput) {"
+    , "    filterInput.addEventListener('input', applyFilter);"
+    , "  }"
+    , "  for (const details of content.querySelectorAll('details')) {"
+    , "    details.addEventListener('toggle', scheduleUpdate);"
+    , "  }"
+    , ""
+    , "  toc.addEventListener('click', (event) => {"
+    , "    const link = event.target.closest('a[href^=\"#\"]');"
+    , "    if (!link || !tocList.contains(link)) return;"
+    , "    const targetId = decodeURIComponent(link.hash.slice(1));"
+    , "    if (!scrollToTarget(targetId)) return;"
+    , "    event.preventDefault();"
+    , "    suspendUntil = 0;"
+    , "    if (location.hash !== '#' + targetId) {"
+    , "      try {"
+    , "        history.pushState(null, '', '#' + targetId);"
+    , "      } catch (_error) {"
+    , "        location.hash = targetId;"
+    , "      }"
+    , "    }"
+    , "  });"
+    , ""
+    , "  window.addEventListener('hashchange', () => {"
+    , "    if (location.hash.length <= 1) return;"
+    , "    const hashTarget = decodeURIComponent(location.hash.slice(1));"
+    , "    if (!scrollToTarget(hashTarget)) scheduleUpdate();"
+    , "  });"
+    , ""
+    , "  if (location.hash.length > 1) {"
+    , "    const hashTarget = decodeURIComponent(location.hash.slice(1));"
+    , "    window.requestAnimationFrame(() => {"
+    , "      applyFilter();"
+    , "      if (!scrollToTarget(hashTarget)) scheduleUpdate();"
+    , "    });"
+    , "    return;"
+    , "  }"
+    , ""
+    , "  applyFilter();"
+    , "  scheduleUpdate();"
+    , "})();"
+    ]
+
+referencePreviewScript :: Text
+referencePreviewScript = Text.unlines
+    [ "(function () {"
+    , "  const content = document.querySelector('main');"
+    , "  const popup = document.getElementById('reference-preview-popup');"
+    , "  if (!content || !popup) return;"
+    , "  let activeTrigger = null;"
+    , "  let lastPointer = null;"
+    , "  let isPinned = false;"
+    , "  let hideTimer = 0;"
+    , "  const offset = 14;"
+    , "  const margin = 12;"
+    , "  const hideDelay = 180;"
+    , ""
+    , "  const cloneHiddenPreview = (trigger) => {"
+    , "    const previewId = trigger.getAttribute('data-preview-id');"
+    , "    const template = previewId ? document.getElementById(previewId) : null;"
+    , "    if (!template) return null;"
+    , "    const clone = template.cloneNode(true);"
+    , "    clone.removeAttribute('id');"
+    , "    return clone;"
+    , "  };"
+    , ""
+    , "  const buildCurrentPreview = (trigger) => {"
+    , "    const targetId = trigger.getAttribute('data-preview-target-id');"
+    , "    const target = targetId ? document.getElementById(targetId) : null;"
+    , "    if (!target || !content.contains(target)) return null;"
+    , "    const template = document.createElement('div');"
+    , "    template.className = 'reference-preview-template';"
+    , "    const heading = document.createElement('div');"
+    , "    heading.className = 'reference-preview-heading';"
+    , "    const kind = target.getAttribute('data-preview-kind') || 'Reference';"
+    , "    const label = target.getAttribute('data-preview-label') || targetId;"
+    , "    const title = target.getAttribute('data-preview-title');"
+    , "    heading.append(document.createTextNode(kind + ' '));"
+    , "    const code = document.createElement('code');"
+    , "    code.textContent = label;"
+    , "    heading.append(code);"
+    , "    if (title) {"
+    , "      heading.append(document.createTextNode(' (' + title + ')'));"
+    , "    }"
+    , "    template.append(heading);"
+    , "    const body = document.createElement('div');"
+    , "    body.className = 'reference-preview-body';"
+    , "    const statement = document.createElement('div');"
+    , "    statement.className = 'reference-preview-statement';"
+    , "    const head = Array.from(target.children).find((child) => child.localName === 'head-');"
+    , "    const nodes = Array.from(target.childNodes);"
+    , "    const start = head ? nodes.indexOf(head) + 1 : 0;"
+    , "    for (const node of nodes.slice(start)) {"
+    , "      statement.append(node.cloneNode(true));"
+    , "    }"
+    , "    if (!statement.childNodes.length) return null;"
+    , "    body.append(statement);"
+    , "    template.append(body);"
+    , "    return template;"
+    , "  };"
+    , ""
+    , "  const buildMissingPreview = (item) => {"
+    , "    const label = item.getAttribute('data-reference-label') || '';"
+    , "    const template = document.createElement('div');"
+    , "    template.className = 'reference-preview-template';"
+    , "    const heading = document.createElement('div');"
+    , "    heading.className = 'reference-preview-heading';"
+    , "    heading.append(document.createTextNode('Reference '));"
+    , "    const code = document.createElement('code');"
+    , "    code.textContent = label;"
+    , "    heading.append(code);"
+    , "    template.append(heading);"
+    , "    const body = document.createElement('div');"
+    , "    body.className = 'reference-preview-body';"
+    , "    const statement = document.createElement('p');"
+    , "    statement.className = 'reference-preview-statement';"
+    , "    statement.textContent = 'Preview unavailable.';"
+    , "    body.append(statement);"
+    , "    template.append(body);"
+    , "    return template;"
+    , "  };"
+    , ""
+    , "  const linkGroupHeading = (item, template) => {"
+    , "    const href = item.getAttribute('data-preview-link');"
+    , "    if (!href) return template;"
+    , "    const heading = template.querySelector('.reference-preview-heading');"
+    , "    const code = heading ? heading.querySelector('code') : null;"
+    , "    if (!heading || !code || code.closest('a')) return template;"
+    , "    const link = document.createElement('a');"
+    , "    link.href = href;"
+    , "    link.append(code.cloneNode(true));"
+    , "    code.replaceWith(link);"
+    , "    return template;"
+    , "  };"
+    , ""
+    , "  const buildGroupPreview = (trigger) => {"
+    , "    if (!trigger.hasAttribute('data-preview-group')) return null;"
+    , "    const items = Array.from(trigger.querySelectorAll('.reference-preview-group-items > [data-reference-label]'));"
+    , "    if (!items.length) return null;"
+    , "    const template = document.createElement('div');"
+    , "    template.className = 'reference-preview-group-template';"
+    , "    for (const item of items) {"
+    , "      const preview = cloneHiddenPreview(item) || buildCurrentPreview(item) || buildMissingPreview(item);"
+    , "      template.append(linkGroupHeading(item, preview));"
+    , "    }"
+    , "    return template;"
+    , "  };"
+    , ""
+    , "  const previewFor = (trigger) => buildGroupPreview(trigger) || cloneHiddenPreview(trigger) || buildCurrentPreview(trigger);"
+    , ""
+    , "  const clamp = (value, min, max) => Math.min(Math.max(value, min), max);"
+    , "  const findTrigger = (target) => target instanceof Element ? target.closest('[data-preview-group], [data-preview-id], [data-preview-target-id]') : null;"
+    , "  const clearHideTimer = () => {"
+    , "    if (!hideTimer) return;"
+    , "    window.clearTimeout(hideTimer);"
+    , "    hideTimer = 0;"
+    , "  };"
+    , ""
+    , "  const hidePreview = () => {"
+    , "    clearHideTimer();"
+    , "    activeTrigger = null;"
+    , "    lastPointer = null;"
+    , "    isPinned = false;"
+    , "    popup.classList.remove('is-visible');"
+    , "    popup.setAttribute('aria-hidden', 'true');"
+    , "    popup.replaceChildren();"
+    , "  };"
+    , ""
+    , "  const scheduleHide = () => {"
+    , "    if (isPinned) return;"
+    , "    clearHideTimer();"
+    , "    hideTimer = window.setTimeout(() => {"
+    , "      hideTimer = 0;"
+    , "      if (!isPinned) hidePreview();"
+    , "    }, hideDelay);"
+    , "  };"
+    , ""
+    , "  const placePreview = () => {"
+    , "    if (!activeTrigger) return;"
+    , "    const triggerRect = activeTrigger.getBoundingClientRect();"
+    , "    const popupRect = popup.getBoundingClientRect();"
+    , "    const fallbackWidth = Math.min(704, Math.max(0, window.innerWidth - margin * 2));"
+    , "    const popupWidth = popupRect.width || fallbackWidth;"
+    , "    const popupHeight = popupRect.height || 0;"
+    , "    const pointer = lastPointer;"
+    , "    const anchorX = pointer ? pointer.clientX : triggerRect.left;"
+    , "    const anchorY = pointer ? pointer.clientY : triggerRect.bottom;"
+    , "    let left = anchorX + (pointer ? offset : 0);"
+    , "    let top = anchorY + offset;"
+    , "    if (top + popupHeight + margin > window.innerHeight) {"
+    , "      const upperAnchor = pointer ? pointer.clientY : triggerRect.top;"
+    , "      top = Math.max(margin, upperAnchor - popupHeight - offset);"
+    , "    }"
+    , "    left = clamp(left, margin, Math.max(margin, window.innerWidth - popupWidth - margin));"
+    , "    popup.style.left = `${left}px`;"
+    , "    popup.style.top = `${top}px`;"
+    , "  };"
+    , ""
+    , "  const showPreview = (trigger, pointerEvent, pinned = false) => {"
+    , "    const source = previewFor(trigger);"
+    , "    if (!source) {"
+    , "      hidePreview();"
+    , "      return;"
+    , "    }"
+    , "    const wasPinned = isPinned && trigger === activeTrigger;"
+    , "    clearHideTimer();"
+    , "    activeTrigger = trigger;"
+    , "    lastPointer = pointerEvent ? { clientX: pointerEvent.clientX, clientY: pointerEvent.clientY } : null;"
+    , "    isPinned = pinned || wasPinned;"
+    , "    popup.replaceChildren(source);"
+    , "    popup.scrollTop = 0;"
+    , "    popup.setAttribute('aria-hidden', 'false');"
+    , "    popup.classList.add('is-visible');"
+    , "    placePreview();"
+    , "  };"
+    , ""
+    , "  content.addEventListener('pointerover', (event) => {"
+    , "    const trigger = findTrigger(event.target);"
+    , "    if (!trigger || !content.contains(trigger) || trigger === activeTrigger) return;"
+    , "    showPreview(trigger, event);"
+    , "  });"
+    , ""
+    , "  content.addEventListener('pointermove', (event) => {"
+    , "    const trigger = findTrigger(event.target);"
+    , "    if (!trigger || trigger !== activeTrigger) return;"
+    , "    if (isPinned) return;"
+    , "    lastPointer = { clientX: event.clientX, clientY: event.clientY };"
+    , "    placePreview();"
+    , "  });"
+    , ""
+    , "  content.addEventListener('pointerout', (event) => {"
+    , "    const trigger = findTrigger(event.target);"
+    , "    if (!trigger || trigger !== activeTrigger) return;"
+    , "    if (isPinned) return;"
+    , "    const related = event.relatedTarget;"
+    , "    if (related instanceof Node && trigger.contains(related)) return;"
+    , "    if (related instanceof Node && popup.contains(related)) return;"
+    , "    scheduleHide();"
+    , "  });"
+    , ""
+    , "  content.addEventListener('focusin', (event) => {"
+    , "    const trigger = findTrigger(event.target);"
+    , "    if (!trigger || !content.contains(trigger)) return;"
+    , "    showPreview(trigger, null);"
+    , "  });"
+    , ""
+    , "  content.addEventListener('focusout', (event) => {"
+    , "    const trigger = findTrigger(event.target);"
+    , "    if (trigger && trigger === activeTrigger && !isPinned) scheduleHide();"
+    , "  });"
+    , ""
+    , "  content.addEventListener('click', (event) => {"
+    , "    const trigger = findTrigger(event.target);"
+    , "    if (!trigger || !trigger.hasAttribute('data-preview-group') || !content.contains(trigger)) return;"
+    , "    event.preventDefault();"
+    , "    showPreview(trigger, event, true);"
+    , "  });"
+    , ""
+    , "  popup.addEventListener('pointerenter', clearHideTimer);"
+    , "  popup.addEventListener('pointerleave', scheduleHide);"
+    , ""
+    , "  document.addEventListener('click', (event) => {"
+    , "    if (!isPinned) return;"
+    , "    const target = event.target;"
+    , "    if (target instanceof Node && popup.contains(target)) return;"
+    , "    if (activeTrigger && target instanceof Node && activeTrigger.contains(target)) return;"
+    , "    hidePreview();"
+    , "  });"
+    , ""
+    , "  content.addEventListener('scroll', hidePreview, { passive: true });"
+    , "  window.addEventListener('resize', hidePreview);"
+    , "  window.addEventListener('hashchange', hidePreview);"
+    , "  document.addEventListener('keydown', (event) => {"
+    , "    if (event.key === 'Escape') {"
+    , "      hidePreview();"
+    , "      return;"
+    , "    }"
+    , "    if (event.key !== 'Enter' && event.key !== ' ') return;"
+    , "    const trigger = findTrigger(document.activeElement);"
+    , "    if (!trigger || !trigger.hasAttribute('data-preview-group')) return;"
+    , "    event.preventDefault();"
+    , "    showPreview(trigger, null, true);"
+    , "  });"
+    , "})();"
+    ]
+
+collectReferencedMarkersOfBlock :: Block -> Set Marker
+collectReferencedMarkersOfBlock =
+    collectBlock
+  where
+        collectBlock :: Block -> Set Marker
+        collectBlock = \case
+            BlockProof _start proof _end ->
+                collectProof proof
+            _ ->
+                mempty
+
+        collectProof :: Proof -> Set Marker
+        collectProof = \case
+            Omitted _loc ->
+                mempty
+            Qed _loc justification ->
+                collectJustification justification
+            Contradiction _loc justification ->
+                collectJustification justification
+            ByCase _loc cases ->
+                foldMap collectCase cases
+            ByContradiction _loc proof ->
+                collectProof proof
+            BySetInduction _loc _term proof ->
+                collectProof proof
+            ByOrdInduction _loc proof ->
+                collectProof proof
+            Assume _loc _stmt proof ->
+                collectProof proof
+            FixSymbolic _loc _vars _bound proof ->
+                collectProof proof
+            FixSuchThat _loc _vars _stmt proof ->
+                collectProof proof
+            Calc _loc _maybeQuant calc proof ->
+                collectCalc calc <> collectProof proof
+            TakeVar _loc _vars _bound _stmt justification proof ->
+                collectJustification justification <> collectProof proof
+            TakeNoun _loc _np justification proof ->
+                collectJustification justification <> collectProof proof
+            Have _loc _maybeStmt _stmt justification proof ->
+                collectJustification justification <> collectProof proof
+            Suffices _loc _stmt justification proof ->
+                collectJustification justification <> collectProof proof
+            Subclaim _loc _stmt subproof proof ->
+                collectProof subproof <> collectProof proof
+            Define _loc _var _expr proof ->
+                collectProof proof
+            DefineFunction _loc _fun _arg _value _boundVar _boundExpr proof ->
+                collectProof proof
+            DefineFunctionLocal _loc _fun _arg _target _domVar _codVar _rules proof ->
+                collectProof proof
+
+        collectCase :: Case -> Set Marker
+        collectCase Case{caseProof} =
+            collectProof caseProof
+
+        collectCalc :: Calc -> Set Marker
+        collectCalc = \case
+            Equation _expr steps ->
+                foldMap (collectJustification . snd) steps
+            Biconditionals _formula steps ->
+                foldMap (collectJustification . snd) steps
+
+        collectJustification :: Justification -> Set Marker
+        collectJustification = \case
+            JustificationRef markers ->
+                Set.fromList (toList markers)
+            JustificationSetExt ->
+                mempty
+            JustificationEmpty ->
+                mempty
+            JustificationLocal ->
+                mempty
+
+collectMissingHints :: HintMap -> [Block] -> MissingHintMap
+collectMissingHints hints = foldMap collectBlock
+    where
+        noteMissingHint :: HintCategory -> Marker -> Int -> MissingHintMap
+        noteMissingHint category marker arity =
+            if Map.member (category, marker, arity) hints
+                then mempty
+                else MissingHintMap (Map.singleton category (Set.singleton marker))
+
+        collectBlock :: Block -> MissingHintMap
+        collectBlock = \case
+            BlockAxiom _loc _title _marker axiom ->
+                collectAxiom axiom
+            BlockClaim _kind _loc _title _marker claim ->
+                collectClaim claim
+            BlockProof _start proof _end ->
+                collectProof proof
+            BlockDefn _loc _title _marker defn ->
+                collectDefn defn
+            BlockAbbr _loc _title _marker abbr ->
+                collectAbbreviation abbr
+            BlockData _loc _title _marker datatype ->
+                collectDatatype datatype
+            BlockInductive _loc _title _marker ind ->
+                collectInductive ind
+            BlockSig _loc _title _marker asms sig ->
+                collectAsms asms
+                    <> collectSignature sig
+            BlockStruct _loc _title _marker structDefn ->
+                collectStructDefn structDefn
+
+        collectAxiom :: Axiom -> MissingHintMap
+        collectAxiom (Axiom asms stmt) =
+            collectAsms asms <> collectStmt stmt
+
+        collectClaim :: Claim -> MissingHintMap
+        collectClaim (Claim asms stmt) =
+            collectAsms asms <> collectStmt stmt
+
+        collectDefn :: Defn -> MissingHintMap
+        collectDefn = \case
+            Defn asms defnHead stmt ->
+                collectAsms asms
+                    <> collectDefnHead defnHead
+                    <> collectStmt stmt
+            DefnFun asms _fun maybeTerm resultTerm ->
+                collectAsms asms
+                    <> foldMap collectTerm maybeTerm
+                    <> collectTerm resultTerm
+            DefnOp symb expr ->
+                collectSymbolPattern symb
+                    <> collectExpr expr
+
+        collectDefnHead :: DefnHead -> MissingHintMap
+        collectDefnHead = \case
+            DefnAdj maybeNp _var _adj ->
+                foldMap collectNounPhraseMaybe maybeNp
+            DefnVerb maybeNp _var _verb ->
+                foldMap collectNounPhraseMaybe maybeNp
+            DefnNoun _var noun ->
+                collectVarNoun noun
+            DefnSymbolicPredicate _predi marker vars ->
+                noteMissingHint PredicateHint marker (length vars)
+                    <> foldMap (collectExpr . ExprVar) vars
+            DefnRel _x rel params _y ->
+                noteMissingHint RelationHint (relationSymbolMarker rel) (length params)
+
+        collectAbbreviation :: Abbreviation -> MissingHintMap
+        collectAbbreviation = \case
+            AbbreviationAdj _var _adj stmt ->
+                collectStmt stmt
+            AbbreviationVerb _var _verb stmt ->
+                collectStmt stmt
+            AbbreviationNoun _var _noun stmt ->
+                collectStmt stmt
+            AbbreviationRel _x rel params _y stmt ->
+                noteMissingHint RelationHint (relationSymbolMarker rel) (length params)
+                    <> collectStmt stmt
+            AbbreviationFun _fun bodyTerm ->
+                collectTerm bodyTerm
+            AbbreviationEq symb expr ->
+                collectSymbolPattern symb
+                    <> collectExpr expr
+
+        collectDatatype :: Datatype -> MissingHintMap
+        collectDatatype Datatype{..} =
+            collectExpr datatypeHeadExpr
+                <> foldMap collectDatatypeClause datatypeClauses
+
+        collectDatatypeClause :: DatatypeClause -> MissingHintMap
+        collectDatatypeClause DatatypeClause{..} =
+            collectExpr datatypeClauseConstructorExpr
+                <> collectExpr datatypeClauseTargetExpr
+                <> foldMap (collectExpr . snd) datatypeClausePremises
+
+        collectInductive :: Inductive -> MissingHintMap
+        collectInductive Inductive{..} =
+            collectSymbolPattern inductiveSymbolPattern
+                <> collectExpr inductiveDomain
+                <> foldMap collectIntroRule inductiveIntros
+
+        collectIntroRule :: IntroRule -> MissingHintMap
+        collectIntroRule IntroRule{..} =
+            foldMap collectFormula introConditions
+                <> collectFormula introResult
+
+        collectSignature :: Signature -> MissingHintMap
+        collectSignature = \case
+            SignatureAdj _var adj ->
+                collectVarAdj adj
+            SignatureVerb _var verb ->
+                collectVarVerb verb
+            SignatureNoun _var noun ->
+                collectVarNoun noun
+            SignatureSymbolic symb np ->
+                collectSymbolPattern symb
+                    <> collectNounPhraseMaybe np
+
+        collectStructDefn :: StructDefn -> MissingHintMap
+        collectStructDefn StructDefn{structAssumes} =
+            foldMap (collectStmt . snd) structAssumes
+
+        collectProof :: Proof -> MissingHintMap
+        collectProof = \case
+            Omitted _loc ->
+                mempty
+            Qed{} ->
+                mempty
+            Contradiction{} ->
+                mempty
+            ByCase _loc cases ->
+                foldMap collectCase cases
+            ByContradiction _loc proof ->
+                collectProof proof
+            BySetInduction _loc maybeTerm proof ->
+                foldMap collectTerm maybeTerm
+                    <> collectProof proof
+            ByOrdInduction _loc proof ->
+                collectProof proof
+            Assume _loc stmt proof ->
+                collectStmt stmt
+                    <> collectProof proof
+            FixSymbolic _loc _vars bound proof ->
+                collectBound bound
+                    <> collectProof proof
+            FixSuchThat _loc _vars stmt proof ->
+                collectStmt stmt
+                    <> collectProof proof
+            Calc _loc maybeQuant calc proof ->
+                foldMap collectCalcQuantifier maybeQuant
+                    <> collectCalc calc
+                    <> collectProof proof
+            TakeVar _loc _vars bound stmt _justification proof ->
+                collectBound bound
+                    <> collectStmt stmt
+                    <> collectProof proof
+            TakeNoun _loc np _justification proof ->
+                collectNounPhraseList np
+                    <> collectProof proof
+            Have _loc maybeStmt stmt _justification proof ->
+                foldMap collectStmt maybeStmt
+                    <> collectStmt stmt
+                    <> collectProof proof
+            Suffices _loc stmt _justification proof ->
+                collectStmt stmt
+                    <> collectProof proof
+            Subclaim _loc stmt subproof proof ->
+                collectStmt stmt
+                    <> collectProof subproof
+                    <> collectProof proof
+            Define _loc _var expr proof ->
+                collectExpr expr
+                    <> collectProof proof
+            DefineFunction _loc _fun _arg value _boundVar boundExpr proof ->
+                collectExpr value
+                    <> collectExpr boundExpr
+                    <> collectProof proof
+            DefineFunctionLocal _loc _fun _arg _target _domVar _codVar rules proof ->
+                foldMap collectLocalFunctionRule rules
+                    <> collectProof proof
+
+        collectLocalFunctionRule :: (Expr, Formula) -> MissingHintMap
+        collectLocalFunctionRule (ruleTerm, formula) =
+            collectExpr ruleTerm
+                <> collectFormula formula
+
+        collectCase :: Case -> MissingHintMap
+        collectCase Case{caseOf, caseProof} =
+            collectStmt caseOf
+                <> collectProof caseProof
+
+        collectCalcQuantifier :: CalcQuantifier -> MissingHintMap
+        collectCalcQuantifier (CalcQuantifier _vars bound maybeStmt) =
+            collectBound bound
+                <> foldMap collectStmt maybeStmt
+
+        collectCalc :: Calc -> MissingHintMap
+        collectCalc = \case
+            Equation expr steps ->
+                collectExpr expr
+                    <> foldMap (collectExpr . fst) steps
+            Biconditionals phi steps ->
+                collectFormula phi
+                    <> foldMap (collectFormula . fst) steps
+
+        collectStmt :: Stmt -> MissingHintMap
+        collectStmt = \case
+            StmtFormula phi ->
+                collectFormula phi
+            StmtVerbPhrase terms verbPhrase ->
+                collectTerms terms
+                    <> collectVerbPhrase verbPhrase
+            StmtNoun terms np ->
+                collectTerms terms
+                    <> collectNounPhraseMaybe np
+            StmtStruct stmtTerm _structPhrase ->
+                collectTerm stmtTerm
+            StmtNeg _loc stmt ->
+                collectStmt stmt
+            StmtExists _loc np ->
+                collectNounPhraseList np
+            StmtConnected _conn _loc stmt1 stmt2 ->
+                collectStmt stmt1
+                    <> collectStmt stmt2
+            StmtQuantPhrase _loc qp stmt ->
+                collectQuantPhrase qp
+                    <> collectStmt stmt
+            SymbolicQuantified _loc _quant _vars bound suchThat stmt ->
+                collectBound bound
+                    <> foldMap collectStmt suchThat
+                    <> collectStmt stmt
+
+        collectQuantPhrase :: QuantPhrase -> MissingHintMap
+        collectQuantPhrase (QuantPhrase _quant np) =
+            collectNounPhraseList np
+
+        collectAsm :: Asm -> MissingHintMap
+        collectAsm = \case
+            AsmSuppose stmt ->
+                collectStmt stmt
+            AsmLetNoun _vars np ->
+                collectNounPhraseMaybe np
+            AsmLetIn _vars expr ->
+                collectExpr expr
+            AsmLetThe _var fun ->
+                collectFun fun
+            AsmLetEq _var expr ->
+                collectExpr expr
+            AsmLetStruct{} ->
+                mempty
+
+        collectTerm :: Term -> MissingHintMap
+        collectTerm = \case
+            TermExpr expr ->
+                collectExpr expr
+            TermFun fun ->
+                collectFun fun
+            TermIota _loc _var stmt ->
+                collectStmt stmt
+            TermQuantified _quant _loc np ->
+                collectNounPhraseMaybe np
+
+        collectNounPhraseMaybe :: NounPhrase Maybe -> MissingHintMap
+        collectNounPhraseMaybe (NounPhrase ls noun _maybeName rs maybeSuchThat) =
+            collectAdjLs ls
+                <> collectNoun noun
+                <> collectAdjRs rs
+                <> foldMap collectStmt maybeSuchThat
+
+        collectNounPhraseList :: NounPhrase [] -> MissingHintMap
+        collectNounPhraseList (NounPhrase ls noun _names rs maybeSuchThat) =
+            collectAdjLs ls
+                <> collectNoun noun
+                <> collectAdjRs rs
+                <> foldMap collectStmt maybeSuchThat
+
+        collectAdjL :: AdjLOf Term -> MissingHintMap
+        collectAdjL (AdjL _loc _item args) =
+            collectTerms args
+
+        collectAdjR :: AdjROf Term -> MissingHintMap
+        collectAdjR = \case
+            AdjR _loc _item args ->
+                collectTerms args
+            AttrRThat verbPhrase ->
+                collectVerbPhrase verbPhrase
+
+        collectAdj :: AdjOf Term -> MissingHintMap
+        collectAdj (Adj _loc _item args) =
+            collectTerms args
+
+        collectVarAdj :: AdjOf VarSymbol -> MissingHintMap
+        collectVarAdj _adj =
+            mempty
+
+        collectVerb :: VerbOf Term -> MissingHintMap
+        collectVerb (Verb _loc _item args) =
+            collectTerms args
+
+        collectVarVerb :: VerbOf VarSymbol -> MissingHintMap
+        collectVarVerb _verb =
+            mempty
+
+        collectVerbPhrase :: VerbPhrase -> MissingHintMap
+        collectVerbPhrase = \case
+            VPVerb verb ->
+                collectVerb verb
+            VPAdj adjs ->
+                foldMap collectAdj adjs
+            VPVerbNot verb ->
+                collectVerb verb
+            VPAdjNot adjs ->
+                foldMap collectAdj adjs
+
+        collectNoun :: NounOf Term -> MissingHintMap
+        collectNoun (Noun _loc _item args) =
+            collectTerms args
+
+        collectVarNoun :: NounOf VarSymbol -> MissingHintMap
+        collectVarNoun _noun =
+            mempty
+
+        collectFun :: FunOf Term -> MissingHintMap
+        collectFun Fun{funArgs} =
+            collectTerms funArgs
+
+        collectBound :: Bound -> MissingHintMap
+        collectBound = \case
+            Unbounded ->
+                mempty
+            Bounded _loc _sign rel expr ->
+                collectRelation rel
+                    <> collectExpr expr
+
+        collectFormula :: Formula -> MissingHintMap
+        collectFormula = \case
+            FormulaChain chain ->
+                collectChain chain
+            FormulaPredicate _loc _predi marker exprs ->
+                noteMissingHint PredicateHint marker (length exprs)
+                    <> collectExprs exprs
+            Connected _loc _conn phi psi ->
+                collectFormula phi
+                    <> collectFormula psi
+            FormulaNeg _loc phi ->
+                collectFormula phi
+            FormulaQuantified _loc _quant _vars bound phi ->
+                collectBound bound
+                    <> collectFormula phi
+            PropositionalConstant{} ->
+                mempty
+
+        collectChain :: Chain -> MissingHintMap
+        collectChain = \case
+            ChainBase lhs _sign rel rhs ->
+                collectExprs lhs
+                    <> collectRelation rel
+                    <> collectExprs rhs
+            ChainCons lhs _sign rel chain ->
+                collectExprs lhs
+                    <> collectRelation rel
+                    <> collectChain chain
+
+        collectRelation :: Relation -> MissingHintMap
+        collectRelation = \case
+            Relation _loc symbol relParams ->
+                noteMissingHint RelationHint (relationSymbolMarker symbol) (length relParams)
+                    <> collectExprs relParams
+            RelationExpr _loc expr ->
+                collectExpr expr
+
+        collectExpr :: Expr -> MissingHintMap
+        collectExpr = \case
+            ExprVar{} ->
+                mempty
+            ExprInteger{} ->
+                mempty
+            ExprOp _loc item args ->
+                noteMissingHint OperatorHint (mixfixMarker item) (length args)
+                    <> collectExprs args
+            ExprStructOp _loc symb maybeExpr ->
+                noteMissingHint StructOpHint (structMarker symb) (length (maybeToList maybeExpr))
+                    <> foldMap collectExpr maybeExpr
+            ExprFiniteSet _loc exprs ->
+                collectExprs exprs
+            ExprSep _loc _var boundExpr stmt ->
+                collectExpr boundExpr
+                    <> collectStmt stmt
+            ExprReplace _loc expr bounds maybeStmt ->
+                collectExpr expr
+                    <> foldMap (collectExpr . snd) bounds
+                    <> foldMap collectStmt maybeStmt
+            ExprReplacePred _loc _rangeVar _domVar domExpr stmt ->
+                collectExpr domExpr
+                    <> collectStmt stmt
+
+        collectSymbolPattern :: SymbolPattern -> MissingHintMap
+        collectSymbolPattern (SymbolPattern symbol vars) =
+            noteMissingHint OperatorHint (mixfixMarker symbol) (length vars)
+
+        collectAsms :: [Asm] -> MissingHintMap
+        collectAsms =
+            foldMap collectAsm
+
+        collectTerms :: Foldable t => t Term -> MissingHintMap
+        collectTerms =
+            foldMap collectTerm
+
+        collectAdjLs :: [AdjLOf Term] -> MissingHintMap
+        collectAdjLs =
+            foldMap collectAdjL
+
+        collectAdjRs :: [AdjROf Term] -> MissingHintMap
+        collectAdjRs =
+            foldMap collectAdjR
+
+        collectExprs :: Foldable t => t Expr -> MissingHintMap
+        collectExprs =
+            foldMap collectExpr
+
+formatMissingHintWarning :: MissingHintMap -> Maybe Text
+formatMissingHintWarning missingHints
+    | null parts = Nothing
+    | otherwise = Just ("WARNING: missing render hints: " <> Text.intercalate "; " parts)
+    where
+        missingHintMap = unMissingHintMap missingHints
+
+        parts =
+            [ label <> "(" <> Text.intercalate ", " (markerText <$> Set.toAscList markers) <> ")"
+            | (category, label) <- categoryLabels
+            , Just markers <- [Map.lookup category missingHintMap]
+            , not (Set.null markers)
+            ]
+
+        categoryLabels :: [(HintCategory, Text)]
+        categoryLabels =
+            [ (OperatorHint, "operators")
+            , (RelationHint, "relations")
+            , (PredicateHint, "predicates")
+            , (StructOpHint, "structops")
+            ]
+
+
+parseHints :: Text -> HintMap
+parseHints source = Map.fromList (parseLine <$> zip [1 :: Int ..] relevantLines)
+    where
+        relevantLines = [line | line <- Text.lines source, not (Text.all isSpace line)]
+
+        parseLine :: (Int, Text) -> ((HintCategory, Marker, Int), RenderHint)
+        parseLine (lineNo, line) = case Text.splitOn "\t" line of
+            [categoryText, markerName, arityText, templateText] ->
+                let category = parseCategory lineNo categoryText
+                    marker = Marker markerName
+                    arity = parseArity lineNo arityText
+                    template = parseTemplate lineNo templateText
+                in ((category, marker, arity), RenderHint arity template)
+            _ ->
+                error ("Malformed render hint at line " <> show lineNo <> ": expected exactly 4 tab-separated columns")
+
+parseCategory :: Int -> Text -> HintCategory
+parseCategory lineNo = \case
+    "operator" -> OperatorHint
+    "relation" -> RelationHint
+    "predicate" -> PredicateHint
+    "structop" -> StructOpHint
+    other -> error ("Unknown render hint category at line " <> show lineNo <> ": " <> Text.unpack other)
+
+parseArity :: Int -> Text -> Int
+parseArity lineNo text = case reads (Text.unpack text) of
+    [(n, "")] -> n
+    _ -> error ("Malformed render-hint arity at line " <> show lineNo <> ": " <> Text.unpack text)
+
+parseTemplate :: Int -> Text -> [TemplatePiece]
+parseTemplate lineNo template = reverse (flush mempty (go mempty [] template))
+    where
+        go :: Text -> [TemplatePiece] -> Text -> [TemplatePiece]
+        go literal acc rest = case parseSlot rest of
+            Just (slot, rest') ->
+                go mempty (Slot slot : flush literal acc) rest'
+            Nothing -> case Text.uncons rest of
+                Nothing -> flush literal acc
+                Just (c, rest') -> go (Text.snoc literal c) acc rest'
+
+        flush :: Text -> [TemplatePiece] -> [TemplatePiece]
+        flush literal acc
+            | Text.null literal = acc
+            | otherwise = Literal literal : acc
+
+        parseSlot :: Text -> Maybe (Int, Text)
+        parseSlot text = do
+            text' <- Text.stripPrefix "<x" text
+            (digit, rest) <- Text.uncons text'
+            guard (isDigit digit)
+            rest' <- Text.stripPrefix "/>" rest
+            let slot = digitToInt digit
+            guard (slot > 0 && slot <= 9)
+            pure (slot, rest')
+
+        _unusedLineNo = lineNo
+
+
+renderBlock :: HintMap -> ReferenceContext -> BlockRenderInfo -> Html ()
+renderBlock hints references (_index, block, blockId) = case block of
+    BlockAxiom _loc title marker axiom ->
+        renderCustomBlock blockId "axiom-" "Axiom" (Just marker) title (renderAxiom hints axiom)
+    BlockClaim kind _loc title marker claim ->
+        renderCustomBlock blockId (claimKindElement kind) (claimKindPrefix kind) (Just marker) title (renderClaim hints claim)
+    BlockProof _start proof _end ->
+        renderProofBlock hints references proof
+    BlockDefn _loc title marker defn ->
+        renderCustomBlock blockId "definition-" "Definition" (Just marker) title (renderDefn hints defn)
+    BlockAbbr _loc title marker abbr ->
+        renderCustomBlock blockId "abbreviation-" "Abbreviation" (Just marker) title (renderAbbreviation hints abbr)
+    BlockData _loc title marker datatype ->
+        renderCustomBlock blockId "datatype-" "Datatype" (Just marker) title (renderDatatype hints datatype)
+    BlockInductive _loc title marker ind ->
+        renderCustomBlock blockId "inductive-" "Inductive" (Just marker) title (renderInductive hints marker ind)
+    BlockSig _loc title marker asms sig ->
+        renderCustomBlock blockId "signature-" "Signature" (Just marker) title (renderSignatureBlock hints asms sig)
+    BlockStruct _loc title marker structDefn ->
+        renderCustomBlock blockId "struct-" "Structure" (Just marker) title (renderStructDefn hints structDefn)
+
+renderTocEntry :: (Int, Text, Block) -> Html ()
+renderTocEntry (index, blockId, block) =
+    li_ do
+        a_ [href_ (renderUrlFragment blockId)] do
+            span_ (toHtml (blockPrefixText block))
+            case formatMarker (blockMarkerOf block) of
+                Nothing ->
+                    when (blockNeedsIndexLabel block) do
+                        code_ (toHtml (Text.pack (show index)))
+                Just marker ->
+                    code_ (toHtml marker)
+
+includeInToc :: Block -> Bool
+includeInToc = \case
+    BlockProof{} -> False
+    _ -> True
+
+renderCustomBlock :: Text -> Text -> Text -> Maybe Marker -> Maybe BlockTitle -> Html () -> Html ()
+renderCustomBlock blockId name prefix mmarker mtitle body =
+    term name (id_ blockId : previewTargetAttributes prefix mmarker mtitle) do
+        renderBlockLead prefix mmarker mtitle True
+        body
+
+previewTargetAttributes :: Text -> Maybe Marker -> Maybe BlockTitle -> [Attributes]
+previewTargetAttributes prefix mmarker mtitle =
+    case formatMarker mmarker of
+        Nothing ->
+            []
+        Just marker ->
+            [ makeAttributes "data-preview-kind" prefix
+            , makeAttributes "data-preview-label" marker
+            ]
+            <> case formatBlockTitle mtitle of
+                Nothing ->
+                    []
+                Just title ->
+                    [makeAttributes "data-preview-title" title]
+
+renderProofBlock :: HintMap -> ReferenceContext -> Proof -> Html ()
+renderProofBlock hints references proof
+    | proofStepCount proof >= proofCollapseThreshold =
+        term "proof-" do
+            details_ do
+                summary_ (renderBlockLead "Proof" Nothing Nothing False)
+                renderProof hints references proof
+    | otherwise =
+        term "proof-" do
+            renderBlockLead "Proof" Nothing Nothing True
+            renderProof hints references proof
+
+blockAnchorId :: Int -> Block -> Text
+blockAnchorId index block =
+    case formatMarker (blockMarkerOf block) of
+        Just marker -> marker
+        Nothing -> sanitizeIdFragment (Text.toLower (blockPrefixText block) <> "-" <> Text.pack (show index))
+
+sanitizeIdFragment :: Text -> Text
+sanitizeIdFragment =
+    Text.dropWhile (== '-') . Text.map sanitize . Text.toLower
+    where
+        sanitize c
+            | isAlphaNum c = c
+            | c == '-' || c == '_' = c
+            | otherwise = '-'
+
+blockPrefixText :: Block -> Text
+blockPrefixText = \case
+    BlockAxiom{} -> "Axiom"
+    BlockClaim kind _ _ _ _ -> claimKindPrefix kind
+    BlockProof{} -> "Proof"
+    BlockDefn{} -> "Definition"
+    BlockAbbr{} -> "Abbreviation"
+    BlockData{} -> "Datatype"
+    BlockInductive{} -> "Inductive"
+    BlockSig{} -> "Signature"
+    BlockStruct{} -> "Structure"
+
+blockMarkerOf :: Block -> Maybe Marker
+blockMarkerOf = \case
+    BlockAxiom _ _ marker _ -> Just marker
+    BlockClaim _ _ _ marker _ -> Just marker
+    BlockProof{} -> Nothing
+    BlockDefn _ _ marker _ -> Just marker
+    BlockAbbr _ _ marker _ -> Just marker
+    BlockData _ _ marker _ -> Just marker
+    BlockInductive _ _ marker _ -> Just marker
+    BlockSig _ _ marker _ _ -> Just marker
+    BlockStruct _ _ marker _ -> Just marker
+
+blockTitleOf :: Block -> Maybe BlockTitle
+blockTitleOf = \case
+    BlockAxiom _ title _ _ -> title
+    BlockClaim _ _ title _ _ -> title
+    BlockProof{} -> Nothing
+    BlockDefn _ title _ _ -> title
+    BlockAbbr _ title _ _ -> title
+    BlockData _ title _ _ -> title
+    BlockInductive _ title _ _ -> title
+    BlockSig _ title _ _ _ -> title
+    BlockStruct _ title _ _ -> title
+
+blockNeedsIndexLabel :: Block -> Bool
+blockNeedsIndexLabel block = case (formatMarker (blockMarkerOf block), formatBlockTitle (blockTitleOf block)) of
+    (Nothing, Nothing) -> True
+    _ -> False
+
+renderBlockLead :: Text -> Maybe Marker -> Maybe BlockTitle -> Bool -> Html ()
+renderBlockLead prefix mmarker mtitle withTrailingSpace =
+    term "head-" do
+        toHtml prefix
+        case formatMarker mmarker of
+            Nothing -> skip
+            Just marker ->
+                term "id-" (toHtml marker)
+        case formatBlockTitle mtitle of
+            Nothing ->
+                toHtml ("." <> suffix)
+            Just title -> do
+                toHtml (" (" :: Text)
+                term "title-" (toHtml title)
+                toHtml (")." <> suffix)
+    where
+        suffix :: Text
+        suffix
+            | withTrailingSpace = " "
+            | otherwise = ""
+
+formatMarker :: Maybe Marker -> Maybe Text
+formatMarker = \case
+    Nothing -> Nothing
+    Just marker ->
+        let text = Text.strip (markerText marker)
+        in if Text.null text then Nothing else Just text
+
+formatBlockTitle :: Maybe BlockTitle -> Maybe Text
+formatBlockTitle =
+    fmap capitalizeTitle . nonEmptyTitle
+    where
+        nonEmptyTitle = \case
+            Nothing -> Nothing
+            Just toks ->
+                let text = Text.strip (Text.unwords (tokToText <$> toks))
+                in if Text.null text then Nothing else Just text
+
+capitalizeTitle :: Text -> Text
+capitalizeTitle text = case Text.uncons text of
+    Nothing -> text
+    Just (c, rest) -> Text.cons (toUpper c) rest
+
+claimKindElement :: ClaimKind -> Text
+claimKindElement = \case
+    Proposition -> "proposition-"
+    Theorem -> "theorem-"
+    Lemma -> "lemma-"
+    Corollary -> "corollary-"
+    PlainClaim -> "claim-"
+
+claimKindPrefix :: ClaimKind -> Text
+claimKindPrefix = \case
+    Proposition -> "Proposition"
+    Theorem -> "Theorem"
+    Lemma -> "Lemma"
+    Corollary -> "Corollary"
+    PlainClaim -> "Claim"
+
+
+renderAxiom :: HintMap -> Axiom -> Html ()
+renderAxiom hints (Axiom asms stmt) =
+    renderWithAssumptions hints asms stmt
+
+renderClaim :: HintMap -> Claim -> Html ()
+renderClaim hints (Claim asms stmt) =
+    renderWithAssumptions hints asms stmt
+
+renderWithAssumptions :: HintMap -> [Asm] -> Stmt -> Html ()
+renderWithAssumptions hints asms stmt = do
+    case asms of
+        [] -> renderStmtInline hints stmt
+        _ -> do
+            toHtml ("Suppose " :: Text)
+            renderAsmList hints asms
+            toHtml (". Then " :: Text)
+            renderStmtInline hints stmt
+    toHtml ("." :: Text)
+
+renderDefn :: HintMap -> Defn -> Html ()
+renderDefn hints = \case
+    Defn asms headStmt stmt ->
+        do
+            when (not (null asms)) do
+                toHtml ("If " :: Text)
+                renderAsmList hints asms
+                toHtml (", then " :: Text)
+            renderDefnHead hints headStmt
+            toHtml (" iff " :: Text)
+            renderStmtInline hints stmt
+            toHtml ("." :: Text)
+    DefnFun asms fun maybeSymbol resultTerm ->
+        do
+            when (not (null asms)) do
+                toHtml ("If " :: Text)
+                renderAsmList hints asms
+                toHtml (", then " :: Text)
+            renderFunInline renderVarInline fun
+            case maybeSymbol of
+                Nothing -> skip
+                Just symbolicTerm -> do
+                    toHtml (", " :: Text)
+                    renderTermInline hints symbolicTerm
+            toHtml (" is " :: Text)
+            renderTermInline hints resultTerm
+            toHtml ("." :: Text)
+    DefnOp symb expr ->
+        do
+            inlineMath do
+                renderSymbolPatternMath hints symb
+                moText "="
+                renderExprMathRow hints expr
+            toHtml ("." :: Text)
+
+renderDefnHead :: HintMap -> DefnHead -> Html ()
+renderDefnHead hints = \case
+    DefnAdj maybeNp var adj -> do
+        renderTypedVar hints maybeNp var
+        toHtml (" is " :: Text)
+        renderAdjInline renderVarInline adj
+    DefnVerb maybeNp var verb -> do
+        renderTypedVar hints maybeNp var
+        toHtml (" " :: Text)
+        renderVerbInline False renderVarInline verb
+    DefnNoun var noun -> do
+        renderVarInline var
+        toHtml (" is a " :: Text)
+        renderNounInline False renderVarInline noun
+    DefnSymbolicPredicate predi marker vars ->
+        inlineMath
+            ( renderHintedMathRow
+                hints
+                PredicateHint
+                marker
+                (ExprVar <$> toList vars)
+                (renderPrefixPredicateFallback predi (renderVarMath <$> toList vars))
+            )
+    DefnRel x rel params y ->
+        inlineMath (renderRelationApplication hints Positive [ExprVar x] (Relation Nowhere rel [ExprVar p | p <- params]) [ExprVar y])
+
+renderTypedVar :: HintMap -> Maybe (NounPhrase Maybe) -> VarSymbol -> Html ()
+renderTypedVar hints = \case
+    Nothing -> renderVarInline
+    Just np -> \var -> do
+        renderNounPhraseMaybe hints np
+        toHtml (" " :: Text)
+        renderVarInline var
+
+
+renderAbbreviation :: HintMap -> Abbreviation -> Html ()
+renderAbbreviation hints = \case
+    AbbreviationAdj var adj stmt ->
+        do
+            renderVarInline var
+            toHtml (" is " :: Text)
+            renderAdjInline renderVarInline adj
+            toHtml (" stands for " :: Text)
+            renderStmtInline hints stmt
+            toHtml ("." :: Text)
+    AbbreviationVerb var verb stmt ->
+        do
+            renderVarInline var
+            toHtml (" " :: Text)
+            renderVerbInline False renderVarInline verb
+            toHtml (" stands for " :: Text)
+            renderStmtInline hints stmt
+            toHtml ("." :: Text)
+    AbbreviationNoun var noun stmt ->
+        do
+            renderVarInline var
+            toHtml (" is a " :: Text)
+            renderNounInline False renderVarInline noun
+            toHtml (" stands for " :: Text)
+            renderStmtInline hints stmt
+            toHtml ("." :: Text)
+    AbbreviationRel x rel params y stmt ->
+        do
+            inlineMath (renderRelationApplication hints Positive [ExprVar x] (Relation Nowhere rel [ExprVar p | p <- params]) [ExprVar y])
+            toHtml (" stands for " :: Text)
+            renderStmtInline hints stmt
+            toHtml ("." :: Text)
+    AbbreviationFun fun bodyTerm ->
+        do
+            renderFunInline renderVarInline fun
+            toHtml (" stands for " :: Text)
+            renderTermInline hints bodyTerm
+            toHtml ("." :: Text)
+    AbbreviationEq symb expr ->
+        do
+            renderSymbolPatternInline hints symb
+            toHtml (" stands for " :: Text)
+            inlineMath (renderExprMathRow hints expr)
+            toHtml ("." :: Text)
+
+renderDatatype :: HintMap -> Datatype -> Html ()
+renderDatatype hints Datatype{..} = do
+    toHtml ("Datatype of " :: Text)
+    inlineMath (renderExprMathRow hints datatypeHeadExpr)
+    toHtml ("." :: Text)
+    ul_ do
+        traverse_ renderDatatypeClause (toList datatypeClauses)
+    -- Derived facts require checked semantic context.
+    where
+        renderDatatypeClause :: DatatypeClause -> Html ()
+        renderDatatypeClause DatatypeClause{..} = li_ do
+            inlineMath do
+                renderRelationApplication hints Positive [datatypeClauseConstructorExpr] (Relation Nowhere ElementSymbol []) [datatypeClauseTargetExpr]
+            case datatypeClausePremises of
+                [] ->
+                    toHtml ("." :: Text)
+                premises -> do
+                    toHtml (" for " :: Text)
+                    joinHtml (toHtml (" and " :: Text)) (renderDatatypePremise <$> premises)
+                    toHtml ("." :: Text)
+
+        renderDatatypePremise :: (VarSymbol, Expr) -> Html ()
+        renderDatatypePremise (x, domain) =
+            inlineMath (renderRelationApplication hints Positive [ExprVar x] (Relation Nowhere ElementSymbol []) [domain])
+
+exprVar :: Expr -> Maybe VarSymbol
+exprVar = \case
+    ExprVar x ->
+        Just x
+    _ ->
+        Nothing
+
+substituteExpr :: Map.Map VarSymbol Expr -> Expr -> Expr
+substituteExpr env = \case
+    ExprVar x ->
+        fromMaybe (ExprVar x) (Map.lookup x env)
+    ExprInteger loc n ->
+        ExprInteger loc n
+    ExprOp loc symbol args ->
+        ExprOp loc symbol (substituteExpr env <$> args)
+    ExprStructOp loc symbol expr ->
+        ExprStructOp loc symbol (substituteExpr env <$> expr)
+    ExprFiniteSet loc exprs ->
+        ExprFiniteSet loc (substituteExpr env <$> exprs)
+    ExprSep loc x bound stmt ->
+        ExprSep loc x (substituteExpr env bound) stmt
+    ExprReplace loc expr bounds maybeStmt ->
+        ExprReplace loc (substituteExpr env expr) ((\(x, bound) -> (x, substituteExpr env bound)) <$> bounds) maybeStmt
+    ExprReplacePred loc x y expr stmt ->
+        ExprReplacePred loc x y (substituteExpr env expr) stmt
+
+elementOfFormula :: Expr -> Expr -> Formula
+elementOfFormula left right =
+    FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere ElementSymbol []) (right :| []))
+
+semanticSubsetFormula :: Set VarSymbol -> Expr -> Expr -> Formula
+semanticSubsetFormula reserved left right =
+    forallIfNeeded [witnessVar]
+        (impliesFormula
+            (elementOfFormula (ExprVar witnessVar) left)
+            (elementOfFormula (ExprVar witnessVar) right))
+    where
+        witnessVar = freshDatatypeVar (reserved <> Set.fromList (exprVars left <> exprVars right)) "x"
+
+equalsFormula :: Expr -> Expr -> Formula
+equalsFormula left right =
+    FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere EqSymbol []) (right :| []))
+
+impliesFormula :: Formula -> Formula -> Formula
+impliesFormula left right =
+    Connected Nowhere Implication left right
+
+formulaConjunction :: [Formula] -> Formula
+formulaConjunction = \case
+    [] ->
+        PropositionalConstant Nowhere IsTop
+    phi : rest ->
+        foldl' (\left right -> Connected Nowhere Conjunction left right) phi rest
+
+formulaDisjunction :: [Formula] -> Formula
+formulaDisjunction = \case
+    [] ->
+        PropositionalConstant Nowhere IsBottom
+    phi : rest ->
+        foldl' (\left right -> Connected Nowhere Disjunction left right) phi rest
+
+forallIfNeeded :: [VarSymbol] -> Formula -> Formula
+forallIfNeeded [] phi = phi
+forallIfNeeded vars phi =
+    FormulaQuantified Nowhere Universally (NonEmpty.fromList vars) Unbounded phi
+
+existsIfNeeded :: [VarSymbol] -> Formula -> Formula
+existsIfNeeded [] phi = phi
+existsIfNeeded vars phi =
+    FormulaQuantified Nowhere Existentially (NonEmpty.fromList vars) Unbounded phi
+
+impliesFrom :: [Formula] -> Formula -> Formula
+impliesFrom [] conclusion = conclusion
+impliesFrom premises conclusion = impliesFormula (formulaConjunction premises) conclusion
+
+freshDatatypeVar :: Set VarSymbol -> Text -> VarSymbol
+freshDatatypeVar used base =
+    List.head
+        [ NamedVar candidate
+        | candidate <- base : [base <> Text.pack (show n) | n <- [(1 :: Int) ..]]
+        , NamedVar candidate `Set.notMember` used
+        ]
+
+renderInductive :: HintMap -> Marker -> Inductive -> Html ()
+renderInductive hints marker Inductive{..} = do
+    toHtml ("Inductive definition of " :: Text)
+    renderSymbolPatternInline hints inductiveSymbolPattern
+    toHtml (" over " :: Text)
+    inlineMath (renderExprMathRow hints inductiveDomain)
+    toHtml ("." :: Text)
+    ul_ do
+        traverse_ renderIntro (toList inductiveIntros)
+    case inductiveDerivedFacts marker Inductive{..} of
+        [] ->
+            skip
+        derivedFacts ->
+            details_ do
+                summary_ (toHtml ("Derived facts" :: Text))
+                ul_ [class_ "inductive-derived-facts"] do
+                    traverse_ (renderInductiveDerivedFact hints) derivedFacts
+    where
+        renderIntro :: IntroRule -> Html ()
+        renderIntro IntroRule{..} = li_ do
+            case introConditions of
+                [] -> skip
+                _ -> do
+                    toHtml ("If " :: Text)
+                    joinHtml (toHtml (" and " :: Text)) (inlineMath . renderFormulaMath hints <$> introConditions)
+                    toHtml (", then " :: Text)
+            inlineMath (renderFormulaMath hints introResult)
+            toHtml ("." :: Text)
+
+renderInductiveDerivedFact :: HintMap -> InductiveDerivedFact -> Html ()
+renderInductiveDerivedFact hints InductiveDerivedFact{inductiveDerivedFactMarker, inductiveDerivedFactFormula} =
+    li_ (id_ (markerText inductiveDerivedFactMarker) : previewTargetAttributes "Inductive Fact" (Just inductiveDerivedFactMarker) Nothing) do
+        term "head-" do
+            code_ (toHtml (markerText inductiveDerivedFactMarker))
+            toHtml (": " :: Text)
+        inlineMath (renderFormulaMath hints inductiveDerivedFactFormula)
+        toHtml ("." :: Text)
+
+data InductiveDerivedFact = InductiveDerivedFact
+    { inductiveDerivedFactMarker :: Marker
+    , inductiveDerivedFactFormula :: Formula
+    }
+
+data InductiveRenderInfo = InductiveRenderInfo
+    { inductiveFactBaseMarker :: Marker
+    , inductiveRenderParams :: [VarSymbol]
+    , inductiveRenderCarrierExpr :: Expr
+    , inductiveRenderDomainExpr :: Expr
+    , inductiveRenderClauses :: NonEmpty InductiveRenderClause
+    }
+
+data InductiveRenderClause = InductiveRenderClause
+    { inductiveRenderClauseVars :: [VarSymbol]
+    , inductiveRenderClauseConditions :: [InductiveRenderCondition]
+    , inductiveRenderClauseResultExpr :: Expr
+    }
+
+data InductiveRenderCondition
+    = InductiveRenderSideCondition Formula
+    | InductiveRenderRecursiveCondition Expr Expr
+
+inductiveDerivedFacts :: Marker -> Inductive -> [InductiveDerivedFact]
+inductiveDerivedFacts marker inductive = case inductiveRenderInfo marker inductive of
+    Nothing ->
+        []
+    Just info ->
+        inductiveIntroFacts info
+            <> [ InductiveDerivedFact (inductiveDomSubsetMarker info) (inductiveDomSubsetFormula info)
+               , InductiveDerivedFact (inductiveCasesMarker info) (inductiveCasesFormula info)
+               , InductiveDerivedFact (inductiveInductMarker info) (inductiveInductFormula info)
+               ]
+
+inductiveRenderInfo :: Marker -> Inductive -> Maybe InductiveRenderInfo
+inductiveRenderInfo marker Inductive{inductiveSymbolPattern = SymbolPattern inductiveSymbol inductiveParams, inductiveDomain, inductiveIntros} = do
+    inductiveRenderClauses <- traverse (inductiveRenderClause inductiveSymbol inductiveParams) inductiveIntros
+    pure InductiveRenderInfo
+        { inductiveFactBaseMarker = marker
+        , inductiveRenderParams = inductiveParams
+        , inductiveRenderCarrierExpr = ExprOp Nowhere inductiveSymbol (ExprVar <$> inductiveParams)
+        , inductiveRenderDomainExpr = inductiveDomain
+        , inductiveRenderClauses
+        }
+    where
+        inductiveRenderClause :: MixfixItem -> [VarSymbol] -> IntroRule -> Maybe InductiveRenderClause
+        inductiveRenderClause symbol params IntroRule{introConditions, introResult} = do
+            inductiveRenderClauseResultExpr <- inductiveRenderResultExpr symbol params introResult
+            inductiveRenderClauseConditions <- traverse (inductiveRenderCondition symbol params) introConditions
+            let paramSet = Set.fromList params
+                inductiveRenderClauseVars =
+                    List.filter (`Set.notMember` paramSet)
+                        (orderedRenderVars (concatMap formulaVars introConditions <> exprVars inductiveRenderClauseResultExpr))
+            pure InductiveRenderClause
+                { inductiveRenderClauseVars
+                , inductiveRenderClauseConditions
+                , inductiveRenderClauseResultExpr
+                }
+
+inductiveRenderResultExpr :: MixfixItem -> [VarSymbol] -> Formula -> Maybe Expr
+inductiveRenderResultExpr symbol params = \case
+    FormulaChain (ChainBase (resultExpr :| []) Positive (Relation _ ElementSymbol []) (carrierExpr :| []))
+        | sameInductiveCarrierExpr symbol params carrierExpr ->
+            Just resultExpr
+    _ ->
+        Nothing
+
+inductiveRenderCondition :: MixfixItem -> [VarSymbol] -> Formula -> Maybe InductiveRenderCondition
+inductiveRenderCondition symbol params phi
+    | not (formulaMentionsFunction symbol phi) =
+        Just (InductiveRenderSideCondition phi)
+    | otherwise = case phi of
+        FormulaChain (ChainBase (recursiveTerm :| []) Positive (Relation _ ElementSymbol []) (recursiveCarrier :| []))
+            | not (exprMentionsFunction symbol recursiveTerm) ->
+                InductiveRenderRecursiveCondition recursiveTerm <$> replaceCarrierExpr symbol params recursiveCarrier
+        _ ->
+            Nothing
+    where
+        replaceCarrierExpr :: MixfixItem -> [VarSymbol] -> Expr -> Maybe Expr
+        replaceCarrierExpr target targetParams =
+            replaceInductiveCarrierExpr target targetParams (ExprVar "__inductive")
+
+inductiveIntroFacts :: InductiveRenderInfo -> [InductiveDerivedFact]
+inductiveIntroFacts info =
+    [ InductiveDerivedFact (inductiveIntroMarker info index) (inductiveIntroFormula info clause)
+    | (index, clause) <- zip [(1 :: Int) ..] (NonEmpty.toList (inductiveRenderClauses info))
+    ]
+
+inductiveIntroMarker :: InductiveRenderInfo -> Int -> Marker
+inductiveIntroMarker info index =
+    Marker (markerText (inductiveFactBaseMarker info) <> "_intro_" <> Text.pack (show index))
+
+inductiveDomSubsetMarker :: InductiveRenderInfo -> Marker
+inductiveDomSubsetMarker info =
+    Marker (markerText (inductiveFactBaseMarker info) <> "_dom_subset")
+
+inductiveCasesMarker :: InductiveRenderInfo -> Marker
+inductiveCasesMarker info =
+    Marker (markerText (inductiveFactBaseMarker info) <> "_cases")
+
+inductiveInductMarker :: InductiveRenderInfo -> Marker
+inductiveInductMarker info =
+    Marker (markerText (inductiveFactBaseMarker info) <> "_induct")
+
+inductiveIntroFormula :: InductiveRenderInfo -> InductiveRenderClause -> Formula
+inductiveIntroFormula info clause =
+    forallIfNeeded (orderedRenderVars (inductiveRenderParams info <> inductiveRenderClauseVars clause))
+        (impliesFrom premises conclusion)
+    where
+        premises = inductiveRenderConditionFormula info <$> inductiveRenderClauseConditions clause
+        conclusion = elementOfFormula (inductiveRenderClauseResultExpr clause) (inductiveRenderCarrierExpr info)
+
+inductiveDomSubsetFormula :: InductiveRenderInfo -> Formula
+inductiveDomSubsetFormula info =
+    forallIfNeeded (inductiveRenderParams info)
+        (semanticSubsetFormula (inductiveUsedVars info) (inductiveRenderCarrierExpr info) (inductiveRenderDomainExpr info))
+
+inductiveCasesFormula :: InductiveRenderInfo -> Formula
+inductiveCasesFormula info =
+    forallIfNeeded (orderedRenderVars (inductiveRenderParams info <> [witnessVar]))
+        (impliesFormula (elementOfFormula (ExprVar witnessVar) (inductiveRenderCarrierExpr info)) (formulaDisjunction disjuncts))
+    where
+        witnessVar = freshDatatypeVar (inductiveUsedVars info) "x"
+        disjuncts = inductiveCaseDisjunct witnessVar <$> NonEmpty.toList (inductiveRenderClauses info)
+        inductiveCaseDisjunct x clause =
+            existsIfNeeded (inductiveRenderClauseVars clause)
+                (formulaConjunction (premises <> [equalsFormula (ExprVar x) (inductiveRenderClauseResultExpr clause)]))
+            where
+                premises = inductiveRenderConditionFormula info <$> inductiveRenderClauseConditions clause
+
+inductiveInductFormula :: InductiveRenderInfo -> Formula
+inductiveInductFormula info =
+    forallIfNeeded (orderedRenderVars (inductiveRenderParams info <> [subsetVar]))
+        (impliesFrom closures conclusion)
+    where
+        subsetVar = freshDatatypeVar (inductiveUsedVars info) "S"
+        closures = inductiveInductionClosure subsetVar <$> NonEmpty.toList (inductiveRenderClauses info)
+        conclusion =
+            semanticSubsetFormula
+                (Set.insert subsetVar (inductiveUsedVars info))
+                (inductiveRenderCarrierExpr info)
+                (ExprVar subsetVar)
+
+inductiveInductionClosure :: VarSymbol -> InductiveRenderClause -> Formula
+inductiveInductionClosure subsetVar clause =
+    forallIfNeeded (inductiveRenderClauseVars clause) (impliesFrom premises conclusion)
+    where
+        premises = inductiveRenderConditionFormulaAt (ExprVar subsetVar) <$> inductiveRenderClauseConditions clause
+        conclusion = elementOfFormula (inductiveRenderClauseResultExpr clause) (ExprVar subsetVar)
+
+inductiveRenderConditionFormula :: InductiveRenderInfo -> InductiveRenderCondition -> Formula
+inductiveRenderConditionFormula info =
+    inductiveRenderConditionFormulaAt (inductiveRenderCarrierExpr info)
+
+inductiveRenderConditionFormulaAt :: Expr -> InductiveRenderCondition -> Formula
+inductiveRenderConditionFormulaAt replacement = \case
+    InductiveRenderSideCondition phi ->
+        phi
+    InductiveRenderRecursiveCondition recursiveTerm recursiveCarrierTemplate ->
+        elementOfFormula recursiveTerm (substituteExpr (Map.singleton "__inductive" replacement) recursiveCarrierTemplate)
+
+inductiveUsedVars :: InductiveRenderInfo -> Set VarSymbol
+inductiveUsedVars info =
+    Set.fromList
+        ( inductiveRenderParams info
+            <> [ var
+               | clause <- NonEmpty.toList (inductiveRenderClauses info)
+               , var <- inductiveRenderClauseVars clause
+               ]
+        )
+
+sameInductiveCarrierExpr :: MixfixItem -> [VarSymbol] -> Expr -> Bool
+sameInductiveCarrierExpr symbol params = \case
+    ExprOp _ symbol' args ->
+        symbol == symbol'
+            && length params == length args
+            && and (zipWith (\param arg -> exprVar arg == Just param) params args)
+    _ ->
+        False
+
+replaceInductiveCarrierExpr :: MixfixItem -> [VarSymbol] -> Expr -> Expr -> Maybe Expr
+replaceInductiveCarrierExpr symbol params replacement = go
+    where
+        go = \case
+            ExprVar x ->
+                Just (ExprVar x)
+            ExprInteger loc n ->
+                Just (ExprInteger loc n)
+            ExprOp loc symbol' args
+                | sameInductiveCarrierExpr symbol params (ExprOp loc symbol' args) ->
+                    Just replacement
+                | symbol == symbol' ->
+                    Nothing
+                | otherwise ->
+                    ExprOp loc symbol' <$> traverse go args
+            ExprStructOp loc structSymbol expr ->
+                ExprStructOp loc structSymbol <$> traverse go expr
+            ExprFiniteSet loc exprs ->
+                ExprFiniteSet loc <$> traverse go exprs
+            ExprSep{} ->
+                Nothing
+            ExprReplace{} ->
+                Nothing
+            ExprReplacePred{} ->
+                Nothing
+
+formulaMentionsFunction :: MixfixItem -> Formula -> Bool
+formulaMentionsFunction symbol = \case
+    FormulaChain chain ->
+        chainMentionsFunction symbol chain
+    FormulaPredicate _loc _predicate _marker exprs ->
+        any (exprMentionsFunction symbol) exprs
+    Connected _loc _conn left right ->
+        formulaMentionsFunction symbol left || formulaMentionsFunction symbol right
+    FormulaNeg _loc phi ->
+        formulaMentionsFunction symbol phi
+    FormulaQuantified _loc _quant _vars _bound phi ->
+        formulaMentionsFunction symbol phi
+    PropositionalConstant{} ->
+        False
+
+chainMentionsFunction :: MixfixItem -> Chain -> Bool
+chainMentionsFunction symbol = \case
+    ChainBase left _sign relation right ->
+        any (exprMentionsFunction symbol) left || relationMentionsFunction symbol relation || any (exprMentionsFunction symbol) right
+    ChainCons left _sign relation rest ->
+        any (exprMentionsFunction symbol) left || relationMentionsFunction symbol relation || chainMentionsFunction symbol rest
+
+relationMentionsFunction :: MixfixItem -> Relation -> Bool
+relationMentionsFunction symbol = \case
+    Relation _loc _relationSymbol exprs ->
+        any (exprMentionsFunction symbol) exprs
+    RelationExpr _loc expr ->
+        exprMentionsFunction symbol expr
+
+exprMentionsFunction :: MixfixItem -> Expr -> Bool
+exprMentionsFunction symbol = \case
+    ExprVar{} ->
+        False
+    ExprInteger{} ->
+        False
+    ExprOp _loc symbol' args ->
+        symbol == symbol' || any (exprMentionsFunction symbol) args
+    ExprStructOp _loc _structSymbol expr ->
+        maybe False (exprMentionsFunction symbol) expr
+    ExprFiniteSet _loc exprs ->
+        any (exprMentionsFunction symbol) exprs
+    ExprSep _loc _var bound _stmt ->
+        exprMentionsFunction symbol bound
+    ExprReplace _loc expr bounds _maybeStmt ->
+        exprMentionsFunction symbol expr || any (exprMentionsFunction symbol . snd) bounds
+    ExprReplacePred _loc _x _y expr _stmt ->
+        exprMentionsFunction symbol expr
+
+formulaVars :: Formula -> [VarSymbol]
+formulaVars = \case
+    FormulaChain chain ->
+        chainVars chain
+    FormulaPredicate _loc _predicate _marker exprs ->
+        concatMap exprVars exprs
+    Connected _loc _conn left right ->
+        formulaVars left <> formulaVars right
+    FormulaNeg _loc phi ->
+        formulaVars phi
+    FormulaQuantified _loc _quant vars _bound phi ->
+        List.filter (`notElem` toList vars) (formulaVars phi)
+    PropositionalConstant{} ->
+        []
+
+chainVars :: Chain -> [VarSymbol]
+chainVars = \case
+    ChainBase left _sign relation right ->
+        concatMap exprVars (toList left) <> relationVars relation <> concatMap exprVars (toList right)
+    ChainCons left _sign relation rest ->
+        concatMap exprVars (toList left) <> relationVars relation <> chainVars rest
+
+relationVars :: Relation -> [VarSymbol]
+relationVars = \case
+    Relation _loc _relationSymbol exprs ->
+        concatMap exprVars exprs
+    RelationExpr _loc expr ->
+        exprVars expr
+
+exprVars :: Expr -> [VarSymbol]
+exprVars = \case
+    ExprVar x ->
+        [x]
+    ExprInteger{} ->
+        []
+    ExprOp _loc _symbol args ->
+        concatMap exprVars args
+    ExprStructOp _loc _structSymbol expr ->
+        maybe [] exprVars expr
+    ExprFiniteSet _loc exprs ->
+        concatMap exprVars exprs
+    ExprSep _loc x bound _stmt ->
+        List.filter (/= x) (exprVars bound)
+    ExprReplace _loc expr bounds _maybeStmt ->
+        let boundVars = fst <$> toList bounds
+            free = exprVars expr <> concatMap (exprVars . snd) (toList bounds)
+        in List.filter (`notElem` boundVars) free
+    ExprReplacePred _loc x y expr _stmt ->
+        List.filter (\var -> var /= x && var /= y) (exprVars expr)
+
+orderedRenderVars :: [VarSymbol] -> [VarSymbol]
+orderedRenderVars =
+    reverse . snd . foldl' step (Set.empty, [])
+    where
+        step (seen, acc) x
+            | x `Set.member` seen = (seen, acc)
+            | otherwise = (Set.insert x seen, x : acc)
+
+renderSignatureBlock :: HintMap -> [Asm] -> Signature -> Html ()
+renderSignatureBlock hints asms sig = do
+    case asms of
+        [] -> skip
+        _ -> do
+            toHtml ("Assumptions: " :: Text)
+            renderAsmList hints asms
+            toHtml ("." :: Text)
+    when (not (null asms)) do
+        p_ do
+            renderSignature hints sig
+            toHtml ("." :: Text)
+    when (null asms) do
+        renderSignature hints sig
+        toHtml ("." :: Text)
+
+renderSignature :: HintMap -> Signature -> Html ()
+renderSignature hints = \case
+    SignatureAdj var adj -> do
+        renderVarInline var
+        toHtml (" can be " :: Text)
+        renderAdjInline renderVarInline adj
+    SignatureVerb var verb -> do
+        renderVarInline var
+        toHtml (" can " :: Text)
+        renderVerbInline False renderVarInline verb
+    SignatureNoun var noun -> do
+        renderVarInline var
+        toHtml (" is a " :: Text)
+        renderNounInline False renderVarInline noun
+    SignatureSymbolic symb np -> do
+        renderSymbolPatternInline hints symb
+        toHtml (" is a " :: Text)
+        renderNounPhraseMaybe hints np
+
+renderStructDefn :: HintMap -> StructDefn -> Html ()
+renderStructDefn hints StructDefn{..} = do
+    toHtml ("Structure phrase: " :: Text)
+    renderStructPhraseInline structPhrase
+    toHtml ("." :: Text)
+    p_ do
+        toHtml ("Label: " :: Text)
+        renderVarInline structLabel
+        toHtml ("." :: Text)
+    when (not (null structParents)) do
+        p_ do
+            toHtml ("Parents: " :: Text)
+            joinHtml (toHtml (", " :: Text)) (renderStructPhraseInline <$> structParents)
+            toHtml ("." :: Text)
+    when (not (null structFixes)) do
+        p_ do
+            toHtml ("Fixes: " :: Text)
+            inlineMath (joinHtml (moText ",") (renderStructSymbolName <$> structFixes))
+            toHtml ("." :: Text)
+    when (not (null structAssumes)) do
+        ul_ do
+            for_ structAssumes \(marker, stmt) -> li_ do
+                toHtml (markerText marker)
+                toHtml (": " :: Text)
+                renderStmtInline hints stmt
+                toHtml ("." :: Text)
+
+
+buildPreviewMap
+    :: HtmlRenderContext
+    -> Set Marker
+    -> AnchorMap
+    -> HtmlRenderIndex
+    -> Either HtmlRenderContextError PreviewMap
+buildPreviewMap
+        context
+        referencedMarkers
+        anchors
+        (HtmlRenderIndex targetIndex) =
+    Map.fromList <$> traverse makePreviewEntry indexedTargets
+  where
+    targets =
+        List.sortOn targetOrdinal
+            [ indexed
+            | marker <- Set.toList referencedMarkers
+            , marker `Map.notMember` anchors
+            , Just indexed@(IndexedReferenceTarget _ source _target) <-
+                [Map.lookup marker targetIndex]
+            , source /= htmlCurrentSource context
+            ]
+    targetOrdinal (IndexedReferenceTarget ordinal _source _target) =
+        ordinal
+    sourceTarget (IndexedReferenceTarget _ordinal source target) =
+        (source, target)
+    indexedTargets =
+        zip [1 :: Int ..] (sourceTarget <$> targets)
+
+    makePreviewEntry (index, (source, target)) = do
+        previewSourceLabel <-
+            htmlSourceLabel context source
+        previewSourceHref <-
+            htmlSourcePageHref context source
+        previewReferenceHref <-
+            htmlSourceFragmentHref
+                context
+                source
+                (targetAnchorId target)
+        let marker = targetMarker target
+            previewMarker = marker
+            previewKind = targetKind target
+            previewTitle = targetTitle target
+            previewId =
+                "reference-preview-" <> Text.pack (show index)
+            previewBody = targetBody target
+        Right (marker, PreviewEntry{..})
+
+renderPreviewStore :: HintMap -> PreviewMap -> Html ()
+renderPreviewStore hints previews =
+    div_ [class_ "reference-preview-store", makeAttributes "aria-hidden" "true"] do
+        traverse_ (renderPreviewEntry hints) (Map.elems previews)
+
+renderPreviewEntry :: HintMap -> PreviewEntry -> Html ()
+renderPreviewEntry hints PreviewEntry{..} =
+    div_ [id_ previewId, class_ "reference-preview-template"] do
+        div_ [class_ "reference-preview-heading"] do
+            toHtml previewKind
+            toHtml (" " :: Text)
+            code_ (toHtml (markerText previewMarker))
+            case previewTitle of
+                Nothing ->
+                    skip
+                Just title -> do
+                    toHtml (" (" :: Text)
+                    toHtml title
+                    toHtml (")" :: Text)
+        div_ [class_ "reference-preview-source"] do
+            toHtml ("from " :: Text)
+            a_ [href_ previewSourceHref] do
+                code_ (toHtml previewSourceLabel)
+        div_ [class_ "reference-preview-body"] do
+            previewBody hints
+
+renderPreviewBlockBody :: HintMap -> Block -> Html ()
+renderPreviewBlockBody hints = \case
+    BlockAxiom _loc _title _marker axiom ->
+        previewStatement (renderAxiom hints axiom)
+    BlockClaim _kind _loc _title _marker claim ->
+        previewStatement (renderClaim hints claim)
+    BlockDefn _loc _title _marker defn ->
+        previewStatement (renderDefn hints defn)
+    BlockAbbr _loc _title _marker abbr ->
+        previewStatement (renderAbbreviation hints abbr)
+    BlockData _loc _title _marker datatype ->
+        renderDatatype hints datatype
+    BlockInductive _loc _title marker ind ->
+        renderInductive hints marker ind
+    BlockSig _loc _title _marker asms sig ->
+        renderSignatureBlock hints asms sig
+    BlockStruct _loc _title _marker structDefn ->
+        renderStructDefn hints structDefn
+    BlockProof{} ->
+        skip
+
+previewStatement :: Html () -> Html ()
+previewStatement =
+    p_ [class_ "reference-preview-statement"]
+
+referenceTargetsOfBlockRenderInfo :: BlockRenderInfo -> [ReferenceTarget]
+referenceTargetsOfBlockRenderInfo (_index, block, blockId) =
+    maybeToList blockTarget <> inductiveTargets
+    where
+        blockTarget = do
+            marker <- blockMarkerOf block
+            pure ReferenceTarget
+                { targetMarker = marker
+                , targetAnchorId = blockId
+                , targetKind = blockPrefixText block
+                , targetTitle = formatBlockTitle (blockTitleOf block)
+                , targetBody = \hints -> renderPreviewBlockBody hints block
+                }
+
+        inductiveTargets = case block of
+            BlockInductive _loc _title marker inductive ->
+                [ ReferenceTarget
+                    { targetMarker = inductiveDerivedFactMarker
+                    , targetAnchorId = markerText inductiveDerivedFactMarker
+                    , targetKind = "Inductive Fact"
+                    , targetTitle = Nothing
+                    , targetBody = \hints -> previewStatement (inlineMath (renderFormulaMath hints inductiveDerivedFactFormula))
+                    }
+                | InductiveDerivedFact{inductiveDerivedFactMarker, inductiveDerivedFactFormula} <- inductiveDerivedFacts marker inductive
+                ]
+            _ ->
+                []
+
+
+renderProof :: HintMap -> ReferenceContext -> Proof -> Html ()
+renderProof hints references = \case
+    Omitted _loc ->
+        p_ "Omitted."
+    Qed mloc justification ->
+        renderProofTerminal mloc justification
+    Contradiction _loc justification ->
+        p_ do
+            toHtml ("Contradiction" :: Text)
+            renderJustificationSuffix references justification
+            toHtml ("." :: Text)
+    ByCase _loc cases -> do
+        p_ "Proof by cases."
+        term "proof-" (traverse_ (renderCase hints references) cases)
+    ByContradiction _loc proof -> do
+        p_ "Proof by contradiction."
+        term "proof-" (renderProof hints references proof)
+    BySetInduction _loc maybeTerm proof -> do
+        p_ do
+            toHtml ("Proof by set induction" :: Text)
+            case maybeTerm of
+                Nothing -> skip
+                Just targetTerm -> do
+                    toHtml (" on " :: Text)
+                    renderTermInline hints targetTerm
+            toHtml ("." :: Text)
+        term "proof-" (renderProof hints references proof)
+    ByOrdInduction _loc proof -> do
+        p_ "Proof by ordinal induction."
+        term "proof-" (renderProof hints references proof)
+    Assume _loc stmt proof -> do
+        p_ do
+            toHtml ("Assume " :: Text)
+            renderStmtInline hints stmt
+            toHtml ("." :: Text)
+        renderProofContinuation hints references proof
+    FixSymbolic _loc vars bound proof -> do
+        p_ do
+            toHtml ("Fix " :: Text)
+            renderVarListInline vars
+            renderBoundInline hints vars bound
+            toHtml ("." :: Text)
+        renderProofContinuation hints references proof
+    FixSuchThat _loc vars stmt proof -> do
+        p_ do
+            toHtml ("Fix " :: Text)
+            renderVarListInline vars
+            toHtml (" such that " :: Text)
+            renderStmtInline hints stmt
+            toHtml ("." :: Text)
+        renderProofContinuation hints references proof
+    Calc _loc maybeQuant calc proof -> do
+        renderCalc hints references maybeQuant calc
+        renderProofContinuation hints references proof
+    TakeVar _loc vars bound stmt justification proof -> do
+        p_ do
+            toHtml ("Take " :: Text)
+            renderVarListInline vars
+            renderBoundInline hints vars bound
+            toHtml (" such that " :: Text)
+            renderStmtInline hints stmt
+            renderJustificationSuffix references justification
+            toHtml ("." :: Text)
+        renderProofContinuation hints references proof
+    TakeNoun _loc np justification proof -> do
+        p_ do
+            toHtml ("Take " :: Text)
+            renderNounPhraseList hints np
+            renderJustificationSuffix references justification
+            toHtml ("." :: Text)
+        renderProofContinuation hints references proof
+    Have _loc maybeStmt stmt justification proof -> do
+        p_ do
+            case maybeStmt of
+                Nothing
+                    | isImplicitProofEnd proof ->
+                        skip
+                    | otherwise ->
+                        toHtml ("We have " :: Text)
+                Just premise -> do
+                    toHtml ("Since " :: Text)
+                    renderStmtInline hints premise
+                    toHtml (", we have " :: Text)
+            renderStmtInline hints stmt
+            renderJustificationSuffix references justification
+            toHtml ("." :: Text)
+        renderProofContinuation hints references proof
+    Suffices _loc stmt justification proof -> do
+        p_ do
+            toHtml ("It suffices to show that " :: Text)
+            renderStmtInline hints stmt
+            renderJustificationSuffix references justification
+            toHtml ("." :: Text)
+        renderProofContinuation hints references proof
+    Subclaim _loc stmt subproof proof -> do
+        p_ do
+            toHtml ("Show " :: Text)
+            renderStmtInline hints stmt
+            toHtml ("." :: Text)
+        term "proof-" (renderProof hints references subproof)
+        renderProofContinuation hints references proof
+    Define _loc var expr proof -> do
+        p_ do
+            toHtml ("Let " :: Text)
+            renderVarEqInline hints var expr
+            toHtml ("." :: Text)
+        renderProofContinuation hints references proof
+    DefineFunction _loc fun arg value boundVar boundExpr proof -> do
+        p_ do
+            toHtml ("Let " :: Text)
+            renderFunctionEqInline hints fun arg value
+            toHtml (" for " :: Text)
+            renderVarInline boundVar
+            toHtml (" in " :: Text)
+            inlineMath (renderExprMathRow hints boundExpr)
+            toHtml ("." :: Text)
+        renderProofContinuation hints references proof
+    DefineFunctionLocal _loc fun arg _target domVar codVar rules proof -> do
+        p_ do
+            toHtml ("Let " :: Text)
+            renderFunctionCallInline fun arg
+            toHtml (" be locally defined from " :: Text)
+            renderVarInline domVar
+            toHtml (" to " :: Text)
+            renderVarInline codVar
+            toHtml ("." :: Text)
+        ul_ do
+            for_ (toList rules) \(ruleTerm, formula) -> li_ do
+                inlineMath (renderExprMathRow hints ruleTerm)
+                toHtml (" if " :: Text)
+                inlineMath (renderFormulaMath hints formula)
+                toHtml ("." :: Text)
+        renderProofContinuation hints references proof
+
+    where
+        renderProofTerminal :: Maybe Location -> Justification -> Html ()
+        renderProofTerminal mloc justification = case (mloc, justification) of
+            (Nothing, JustificationEmpty) ->
+                skip
+            (Just _, JustificationEmpty) ->
+                p_ "Trivial."
+            _ ->
+                p_ do
+                    toHtml ("Follows" :: Text)
+                    renderJustificationSuffix references justification
+                    toHtml ("." :: Text)
+
+renderProofContinuation :: HintMap -> ReferenceContext -> Proof -> Html ()
+renderProofContinuation hints references proof =
+    unless (isImplicitProofEnd proof) (renderProof hints references proof)
+
+isImplicitProofEnd :: Proof -> Bool
+isImplicitProofEnd = \case
+    Qed Nothing JustificationEmpty -> True
+    _ -> False
+
+proofStepCount :: Proof -> Int
+proofStepCount = \case
+    Omitted _loc -> 1
+    Qed{} -> 1
+    Contradiction{} -> 1
+    ByCase _loc cases -> 1 + sum (caseStepCount <$> cases)
+    ByContradiction _loc proof -> 1 + proofStepCount proof
+    BySetInduction _loc _maybeTerm proof -> 1 + proofStepCount proof
+    ByOrdInduction _loc proof -> 1 + proofStepCount proof
+    Assume _loc _stmt proof -> 1 + proofStepCount proof
+    FixSymbolic _loc _vars _bound proof -> 1 + proofStepCount proof
+    FixSuchThat _loc _vars _stmt proof -> 1 + proofStepCount proof
+    Calc _loc _maybeQuant calc proof -> 1 + calcStepCount calc + proofStepCount proof
+    TakeVar _loc _vars _bound _stmt _justification proof -> 1 + proofStepCount proof
+    TakeNoun _loc _np _justification proof -> 1 + proofStepCount proof
+    Have _loc _maybeStmt _stmt _justification proof -> 1 + proofStepCount proof
+    Suffices _loc _stmt _justification proof -> 1 + proofStepCount proof
+    Subclaim _loc _stmt subproof proof -> 1 + proofStepCount subproof + proofStepCount proof
+    Define _loc _var _expr proof -> 1 + proofStepCount proof
+    DefineFunction _loc _fun _arg _value _boundVar _boundExpr proof -> 1 + proofStepCount proof
+    DefineFunctionLocal _loc _fun _arg _target _domVar _codVar rules proof ->
+        1 + length rules + proofStepCount proof
+
+caseStepCount :: Case -> Int
+caseStepCount Case{caseProof} = 1 + proofStepCount caseProof
+
+calcStepCount :: Calc -> Int
+calcStepCount = \case
+    Equation _ steps -> length steps
+    Biconditionals _ steps -> length steps
+
+renderCase :: HintMap -> ReferenceContext -> Case -> Html ()
+renderCase hints references Case{..} =
+    term "proof-" do
+        p_ do
+            toHtml ("Case " :: Text)
+            renderStmtInline hints caseOf
+            toHtml ("." :: Text)
+        renderProof hints references caseProof
+
+renderCalc :: HintMap -> ReferenceContext -> Maybe CalcQuantifier -> Calc -> Html ()
+renderCalc hints references maybeQuant calc = do
+    p_ do
+        toHtml ("Calculation" :: Text)
+        case maybeQuant of
+            Nothing -> skip
+            Just quant -> do
+                toHtml (" for " :: Text)
+                renderCalcQuantifierInline hints quant
+        toHtml ("." :: Text)
+    blockMath (renderCalcMath hints calc)
+    let justifications = calcJustifications calc
+    when (not (null justifications)) do
+        ul_ do
+            traverse_ renderStepJustification justifications
+    where
+        renderStepJustification :: (Int, Justification) -> Html ()
+        renderStepJustification (_idx, JustificationEmpty) = skip
+        renderStepJustification (idx, jst) = li_ do
+            toHtml ("Step " <> Text.pack (show idx) <> ": " :: Text)
+            renderJustification references jst
+            toHtml ("." :: Text)
+
+renderCalcQuantifierInline :: HintMap -> CalcQuantifier -> Html ()
+renderCalcQuantifierInline hints (CalcQuantifier vars bound maybeStmt) = do
+    renderVarListInline vars
+    renderBoundInline hints vars bound
+    case maybeStmt of
+        Nothing -> skip
+        Just stmt -> do
+            toHtml (" such that " :: Text)
+            renderStmtInline hints stmt
+
+renderCalcMath :: HintMap -> Calc -> Html ()
+renderCalcMath hints = \case
+    Equation expr steps -> do
+        renderExprMathRow hints expr
+        for_ (toList steps) \(nextExpr, _jst) -> do
+            moText "="
+            renderExprMathRow hints nextExpr
+    Biconditionals phi steps -> do
+        renderFormulaMath hints phi
+        for_ (toList steps) \(nextPhi, _jst) -> do
+            moText "⇔"
+            renderFormulaMath hints nextPhi
+
+calcJustifications :: Calc -> [(Int, Justification)]
+calcJustifications = \case
+    Equation _ steps ->
+        zip [1..] (snd <$> toList steps)
+    Biconditionals _ steps ->
+        zip [1..] (snd <$> toList steps)
+
+
+renderStmtInline :: HintMap -> Stmt -> Html ()
+renderStmtInline hints = \case
+    StmtFormula phi ->
+        inlineMath (renderFormulaMath hints phi)
+    StmtVerbPhrase ts vp -> do
+        renderTermList hints ts
+        toHtml (" " :: Text)
+        renderVerbPhraseInline hints (length ts > 1) vp
+    StmtNoun ts np -> do
+        renderTermList hints ts
+        toHtml (if length ts > 1 then " are a " else " is a " :: Text)
+        renderNounPhraseMaybe hints np
+    StmtStruct t structPhrase -> do
+        renderTermInline hints t
+        toHtml (" is a " :: Text)
+        renderStructPhraseInline structPhrase
+    StmtNeg _loc stmt -> do
+        toHtml ("it is not the case that " :: Text)
+        renderStmtInline hints stmt
+    StmtExists _loc np -> do
+        toHtml ("there exists " :: Text)
+        renderNounPhraseList hints np
+    StmtConnected conn _loc stmt1 stmt2 -> do
+        renderConnectedStmtInline hints conn stmt1 stmt2
+    StmtQuantPhrase _loc qp stmt -> do
+        renderQuantPhraseInline hints qp
+        toHtml (" " :: Text)
+        renderStmtInline hints stmt
+    SymbolicQuantified _loc quant vars bound suchThat stmt -> do
+        toHtml (quantifierWord quant)
+        toHtml (" " :: Text)
+        renderBoundSubjectInline hints vars bound
+        renderQuantifiedTailInline hints quant suchThat stmt
+
+renderQuantPhraseInline :: HintMap -> QuantPhrase -> Html ()
+renderQuantPhraseInline hints (QuantPhrase quant np) = do
+    toHtml (quantifierWord quant)
+    toHtml (" " :: Text)
+    renderNounPhraseList hints np
+
+quantifierWord :: Quantifier -> Text
+quantifierWord = \case
+    Universally -> "for every"
+    Existentially -> "there exists"
+    Nonexistentially -> "there exists no"
+
+connectiveWord :: Connective -> Text
+connectiveWord = \case
+    Conjunction -> "and"
+    Disjunction -> "or"
+    Implication -> "implies"
+    Equivalence -> "iff"
+    ExclusiveOr -> "xor"
+    NegatedDisjunction -> "nor"
+
+renderConnectedStmtInline :: HintMap -> Connective -> Stmt -> Stmt -> Html ()
+renderConnectedStmtInline hints conn stmt1 stmt2 = case conn of
+    ExclusiveOr -> do
+        toHtml ("either " :: Text)
+        renderStmtInline hints stmt1
+        toHtml (" or " :: Text)
+        renderStmtInline hints stmt2
+    NegatedDisjunction -> do
+        toHtml ("neither " :: Text)
+        renderStmtInline hints stmt1
+        toHtml (" nor " :: Text)
+        renderStmtInline hints stmt2
+    _ -> do
+        renderStmtInline hints stmt1
+        toHtml (" " :: Text)
+        toHtml (connectiveWord conn)
+        toHtml (" " :: Text)
+        renderStmtInline hints stmt2
+
+renderQuantifiedTailInline :: HintMap -> Quantifier -> Maybe Stmt -> Stmt -> Html ()
+renderQuantifiedTailInline hints quant suchThat stmt =
+    case quant of
+        Universally -> do
+            for_ suchThat \suchStmt -> do
+                toHtml (" such that " :: Text)
+                renderStmtInline hints suchStmt
+            toHtml (" we have " :: Text)
+            renderStmtInline hints stmt
+        Existentially ->
+            renderExistentialTailInline hints suchThat stmt
+        Nonexistentially ->
+            renderExistentialTailInline hints suchThat stmt
+
+renderExistentialTailInline :: HintMap -> Maybe Stmt -> Stmt -> Html ()
+renderExistentialTailInline hints suchThat stmt = do
+    toHtml (" such that " :: Text)
+    case suchThat of
+        Nothing ->
+            renderStmtInline hints stmt
+        Just suchStmt -> do
+            renderStmtInline hints suchStmt
+            toHtml (" and " :: Text)
+            renderStmtInline hints stmt
+
+
+renderAsmList :: HintMap -> [Asm] -> Html ()
+renderAsmList hints asms =
+    joinHtml (toHtml ("; " :: Text)) (renderAsm hints <$> asms)
+
+renderAsm :: HintMap -> Asm -> Html ()
+renderAsm hints = \case
+    AsmSuppose stmt ->
+        renderStmtInline hints stmt
+    AsmLetNoun vars np -> do
+        renderVarListInline vars
+        toHtml (" be " :: Text)
+        renderNounPhraseMaybe hints np
+    AsmLetIn vars expr -> do
+        renderVarListInline vars
+        toHtml (" be in " :: Text)
+        inlineMath (renderExprMathRow hints expr)
+    AsmLetThe var fun -> do
+        renderVarInline var
+        toHtml (" be " :: Text)
+        renderFunInline renderTermInline' fun
+            where renderTermInline' = renderTermInline hints
+    AsmLetEq var expr -> do
+        renderVarEqInline hints var expr
+    AsmLetStruct var structPhrase -> do
+        renderVarInline var
+        toHtml (" be a " :: Text)
+        renderStructPhraseInline structPhrase
+
+
+renderTermInline :: HintMap -> Term -> Html ()
+renderTermInline hints = \case
+    TermExpr expr ->
+        inlineMath (renderExprMathRow hints expr)
+    TermFun fun -> do
+        toHtml ("the " :: Text)
+        renderFunInline (renderTermInline hints) fun
+    TermIota _loc var stmt -> do
+        toHtml ("the " :: Text)
+        renderVarInline var
+        toHtml (" such that " :: Text)
+        renderStmtInline hints stmt
+    TermQuantified quant _loc np -> do
+        toHtml (termQuantifierWord quant)
+        toHtml (" " :: Text)
+        renderNounPhraseMaybe hints np
+
+termQuantifierWord :: Quantifier -> Text
+termQuantifierWord = \case
+    Universally -> "every"
+    Existentially -> "some"
+    Nonexistentially -> "no"
+
+renderTermList :: HintMap -> NonEmpty Term -> Html ()
+renderTermList hints =
+    joinHtml (toHtml (" and " :: Text)) . fmap (renderTermInline hints) . toList
+
+renderNounPhraseMaybe :: HintMap -> NounPhrase Maybe -> Html ()
+renderNounPhraseMaybe hints (NounPhrase ls noun maybeName rs maybeSuchThat) = do
+    renderAdjListInline renderTermInline' ls
+    renderNounInline False renderTermInline' noun
+    case maybeName of
+        Nothing -> skip
+        Just name -> do
+            toHtml (" " :: Text)
+            renderVarInline name
+    renderAdjRListInline hints rs
+    case maybeSuchThat of
+        Nothing -> skip
+        Just stmt -> do
+            toHtml (" such that " :: Text)
+            renderStmtInline hints stmt
+    where
+        renderTermInline' = renderTermInline hints
+
+renderNounPhraseList :: HintMap -> NounPhrase [] -> Html ()
+renderNounPhraseList hints (NounPhrase ls noun names rs maybeSuchThat) = do
+    renderAdjListInline renderTermInline' ls
+    renderNounInline (length names > 1) renderTermInline' noun
+    when (not (null names)) do
+        toHtml (" " :: Text)
+        renderVarListInline (NonEmpty.fromList names)
+    renderAdjRListInline hints rs
+    case maybeSuchThat of
+        Nothing -> skip
+        Just stmt -> do
+            toHtml (" such that " :: Text)
+            renderStmtInline hints stmt
+    where
+        renderTermInline' = renderTermInline hints
+
+renderAdjListInline :: (a -> Html ()) -> [AdjLOf a] -> Html ()
+renderAdjListInline renderArg adjs =
+    unless (null adjs) do
+        joinHtml (toHtml (" " :: Text)) (renderAdjLInline renderArg <$> adjs)
+        toHtml (" " :: Text)
+
+renderAdjRListInline :: HintMap -> [AdjROf Term] -> Html ()
+renderAdjRListInline hints adjs =
+    unless (null adjs) do
+        toHtml (" " :: Text)
+        joinHtml (toHtml (" and " :: Text)) (renderAdjRInline hints <$> adjs)
+
+renderAdjLInline :: (a -> Html ()) -> AdjLOf a -> Html ()
+renderAdjLInline renderArg (AdjL _loc item args) =
+    renderLexicalItemInline renderArg item args
+
+renderAdjRInline :: HintMap -> AdjROf Term -> Html ()
+renderAdjRInline hints = \case
+    AdjR _loc item args ->
+        renderLexicalItemInline (renderTermInline hints) item args
+    AttrRThat verbPhrase -> do
+        toHtml ("that " :: Text)
+        renderVerbPhraseInline hints False verbPhrase
+
+renderAdjInline :: (a -> Html ()) -> AdjOf a -> Html ()
+renderAdjInline renderArg (Adj _loc item args) =
+    renderLexicalItemInline renderArg item args
+
+renderVerbInline :: Bool -> (a -> Html ()) -> VerbOf a -> Html ()
+renderVerbInline isPlural renderArg (Verb _loc item args) =
+    renderLexicalItemSgPlInline isPlural renderArg item args
+
+renderVerbPhraseInline :: HintMap -> Bool -> VerbPhrase -> Html ()
+renderVerbPhraseInline hints isPlural = \case
+    VPVerb verb ->
+        renderVerbInline isPlural (renderTermInline hints) verb
+    VPAdj adjs -> do
+        toHtml (if isPlural then "are " else "is " :: Text)
+        joinHtml (toHtml (" and " :: Text)) (renderAdjInline (renderTermInline hints) <$> toList adjs)
+    VPVerbNot verb -> do
+        toHtml (if isPlural then "do not " else "does not " :: Text)
+        renderVerbInline True (renderTermInline hints) verb
+    VPAdjNot adjs -> do
+        toHtml (if isPlural then "are not " else "is not " :: Text)
+        joinHtml (toHtml (" and " :: Text)) (renderAdjInline (renderTermInline hints) <$> toList adjs)
+
+renderNounInline :: Bool -> (a -> Html ()) -> NounOf a -> Html ()
+renderNounInline isPlural renderArg (Noun _loc item args) =
+    renderLexicalItemSgPlInline isPlural renderArg item args
+
+renderFunInline :: (a -> Html ()) -> FunOf a -> Html ()
+renderFunInline renderArg Fun{phrase, funArgs} =
+    renderLexicalItemSgPlInline False renderArg phrase funArgs
+
+renderStructPhraseInline :: StructPhrase -> Html ()
+renderStructPhraseInline item =
+    renderLexicalItemSgPlInline False renderTermInlinePlaceholder item []
+
+renderTermInlinePlaceholder :: a -> Html ()
+renderTermInlinePlaceholder _ = toHtml ("?" :: Text)
+
+renderLexicalItemInline :: (a -> Html ()) -> LexicalItem -> [a] -> Html ()
+renderLexicalItemInline renderArg item args =
+    renderPatternInline renderArg (lexicalItemPhrase item) args
+
+renderLexicalItemSgPlInline :: Bool -> (a -> Html ()) -> LexicalItemSgPl -> [a] -> Html ()
+renderLexicalItemSgPlInline isPlural renderArg item args =
+    renderPatternInline renderArg phrase args
+    where
+        phrase = if isPlural then pl (lexicalItemSgPlPhrase item) else sg (lexicalItemSgPlPhrase item)
+
+renderPatternInline :: (a -> Html ()) -> [Maybe Token] -> [a] -> Html ()
+renderPatternInline renderArg patternParts args =
+    joinHtml (toHtml (" " :: Text)) (go patternParts args)
+    where
+        go [] [] = []
+        go [] (_ : _) = error "renderPatternInline: too many arguments"
+        go (Nothing : rest) (arg : restArgs) = renderArg arg : go rest restArgs
+        go (Nothing : _) [] = error "renderPatternInline: not enough arguments"
+        go (Just tok : rest) restArgs = tokenTextHtml tok : go rest restArgs
+
+renderStmtMath :: HintMap -> Stmt -> Html ()
+renderStmtMath hints =
+    renderStmtMathFragments . stmtMathFragments hints
+
+renderStmtMathFragments :: StmtMathFragments -> Html ()
+renderStmtMathFragments =
+    go ""
+    where
+        go :: Text -> StmtMathFragments -> Html ()
+        go pending = \case
+            [] ->
+                flush pending
+            StmtMathProse text : rest ->
+                go (pending <> text) rest
+            StmtMathNode node : rest -> do
+                flush pending
+                node
+                go "" rest
+
+        flush :: Text -> Html ()
+        flush text =
+            let renderedText = preserveBoundarySpaces text
+            in unless (Text.null renderedText) (mtextText renderedText)
+
+        preserveBoundarySpaces :: Text -> Text
+        preserveBoundarySpaces text =
+            Text.replicate leadingCount nbsp
+                <> middleText
+                <> Text.replicate trailingCount nbsp
+            where
+                leadingCount = Text.length (Text.takeWhile (== ' ') text)
+                textAfterLeading = Text.drop leadingCount text
+                trailingCount = Text.length (Text.takeWhileEnd (== ' ') textAfterLeading)
+                middleText = Text.dropEnd trailingCount textAfterLeading
+                nbsp = Text.singleton '\160'
+
+stmtMathProse :: Text -> StmtMathFragments
+stmtMathProse text
+    | Text.null text = []
+    | otherwise = [StmtMathProse text]
+
+stmtMathNode :: Html () -> StmtMathFragments
+stmtMathNode html =
+    [StmtMathNode html]
+
+joinStmtMathFragments :: StmtMathFragments -> [StmtMathFragments] -> StmtMathFragments
+joinStmtMathFragments _ [] = []
+joinStmtMathFragments separator (first : rest) =
+    first <> foldMap (separator <>) rest
+
+stmtMathFragments :: HintMap -> Stmt -> StmtMathFragments
+stmtMathFragments hints = \case
+    StmtFormula phi ->
+        stmtMathNode (renderFormulaMath hints phi)
+    StmtVerbPhrase ts vp -> do
+        termListMathFragments hints ts
+            <> stmtMathProse " "
+            <> verbPhraseMathFragments hints (length ts > 1) vp
+    StmtNoun ts np -> do
+        termListMathFragments hints ts
+            <> stmtMathProse (if length ts > 1 then " are a " else " is a ")
+            <> nounPhraseMaybeMathFragments hints np
+    StmtStruct t structPhrase -> do
+        termMathFragments hints t
+            <> stmtMathProse " is a "
+            <> structPhraseMathFragments structPhrase
+    StmtNeg _loc stmt -> do
+        stmtMathProse "it is not the case that "
+            <> stmtMathFragments hints stmt
+    StmtExists _loc np -> do
+        stmtMathProse "there exists "
+            <> nounPhraseListMathFragments hints np
+    StmtConnected conn _loc stmt1 stmt2 -> do
+        connectedStmtMathFragments hints conn stmt1 stmt2
+    StmtQuantPhrase _loc qp stmt -> do
+        quantPhraseMathFragments hints qp
+            <> stmtMathProse " "
+            <> stmtMathFragments hints stmt
+    SymbolicQuantified _loc quant vars bound suchThat stmt -> do
+        stmtMathProse (quantifierWord quant <> " ")
+            <> boundSubjectMathFragments hints vars bound
+            <> quantifiedTailMathFragments hints quant suchThat stmt
+
+quantPhraseMathFragments :: HintMap -> QuantPhrase -> StmtMathFragments
+quantPhraseMathFragments hints (QuantPhrase quant np) =
+    stmtMathProse (quantifierWord quant <> " ")
+        <> nounPhraseListMathFragments hints np
+
+connectedStmtMathFragments :: HintMap -> Connective -> Stmt -> Stmt -> StmtMathFragments
+connectedStmtMathFragments hints conn stmt1 stmt2 = case conn of
+    ExclusiveOr ->
+        stmtMathProse "either "
+            <> stmtMathFragments hints stmt1
+            <> stmtMathProse " or "
+            <> stmtMathFragments hints stmt2
+    NegatedDisjunction ->
+        stmtMathProse "neither "
+            <> stmtMathFragments hints stmt1
+            <> stmtMathProse " nor "
+            <> stmtMathFragments hints stmt2
+    _ ->
+        stmtMathFragments hints stmt1
+            <> stmtMathProse (" " <> connectiveWord conn <> " ")
+            <> stmtMathFragments hints stmt2
+
+quantifiedTailMathFragments :: HintMap -> Quantifier -> Maybe Stmt -> Stmt -> StmtMathFragments
+quantifiedTailMathFragments hints quant suchThat stmt =
+    case quant of
+        Universally ->
+            foldMap
+                (\suchStmt -> stmtMathProse " such that " <> stmtMathFragments hints suchStmt)
+                suchThat
+                <> stmtMathProse " we have "
+                <> stmtMathFragments hints stmt
+        Existentially ->
+            existentialTailMathFragments hints suchThat stmt
+        Nonexistentially ->
+            existentialTailMathFragments hints suchThat stmt
+
+existentialTailMathFragments :: HintMap -> Maybe Stmt -> Stmt -> StmtMathFragments
+existentialTailMathFragments hints suchThat stmt =
+    stmtMathProse " such that "
+        <> case suchThat of
+            Nothing ->
+                stmtMathFragments hints stmt
+            Just suchStmt ->
+                stmtMathFragments hints suchStmt
+                    <> stmtMathProse " and "
+                    <> stmtMathFragments hints stmt
+
+termMathFragments :: HintMap -> Term -> StmtMathFragments
+termMathFragments hints = \case
+    TermExpr expr ->
+        stmtMathNode (renderExprMathRow hints expr)
+    TermFun fun -> do
+        stmtMathProse "the "
+            <> funMathFragments (termMathFragments hints) fun
+    TermIota _loc var stmt -> do
+        stmtMathProse "the "
+            <> stmtMathNode (renderVarMath var)
+            <> stmtMathProse " such that "
+            <> stmtMathFragments hints stmt
+    TermQuantified quant _loc np -> do
+        stmtMathProse (termQuantifierWord quant <> " ")
+            <> nounPhraseMaybeMathFragments hints np
+
+termListMathFragments :: HintMap -> NonEmpty Term -> StmtMathFragments
+termListMathFragments hints =
+    joinStmtMathFragments (stmtMathProse " and ") . fmap (termMathFragments hints) . toList
+
+nounPhraseMaybeMathFragments :: HintMap -> NounPhrase Maybe -> StmtMathFragments
+nounPhraseMaybeMathFragments hints (NounPhrase ls noun maybeName rs maybeSuchThat) =
+    adjListMathFragments renderTermMath' ls
+        <> nounMathFragments False renderTermMath' noun
+        <> foldMap (\name -> stmtMathProse " " <> stmtMathNode (renderVarMath name)) maybeName
+        <> adjRListMathFragments hints rs
+        <> foldMap (\stmt -> stmtMathProse " such that " <> stmtMathFragments hints stmt) maybeSuchThat
+    where
+        renderTermMath' = termMathFragments hints
+
+nounPhraseListMathFragments :: HintMap -> NounPhrase [] -> StmtMathFragments
+nounPhraseListMathFragments hints (NounPhrase ls noun names rs maybeSuchThat) =
+    adjListMathFragments renderTermMath' ls
+        <> nounMathFragments (length names > 1) renderTermMath' noun
+        <> if null names
+            then []
+            else stmtMathProse " " <> stmtMathNode (renderVarListMath (NonEmpty.fromList names))
+        <> adjRListMathFragments hints rs
+        <> foldMap (\stmt -> stmtMathProse " such that " <> stmtMathFragments hints stmt) maybeSuchThat
+    where
+        renderTermMath' = termMathFragments hints
+
+adjListMathFragments :: (a -> StmtMathFragments) -> [AdjLOf a] -> StmtMathFragments
+adjListMathFragments renderArg adjs =
+    if null adjs
+        then []
+        else joinStmtMathFragments (stmtMathProse " ") (renderAdjLMathFragments renderArg <$> adjs)
+            <> stmtMathProse " "
+
+adjRListMathFragments :: HintMap -> [AdjROf Term] -> StmtMathFragments
+adjRListMathFragments hints adjs =
+    if null adjs
+        then []
+        else stmtMathProse " "
+            <> joinStmtMathFragments (stmtMathProse " and ") (renderAdjRMathFragments hints <$> adjs)
+
+renderAdjLMathFragments :: (a -> StmtMathFragments) -> AdjLOf a -> StmtMathFragments
+renderAdjLMathFragments renderArg (AdjL _loc item args) =
+    lexicalItemStmtMathFragments renderArg item args
+
+renderAdjRMathFragments :: HintMap -> AdjROf Term -> StmtMathFragments
+renderAdjRMathFragments hints = \case
+    AdjR _loc item args ->
+        lexicalItemStmtMathFragments (termMathFragments hints) item args
+    AttrRThat verbPhrase ->
+        stmtMathProse "that "
+            <> verbPhraseMathFragments hints False verbPhrase
+
+adjMathFragments :: (a -> StmtMathFragments) -> AdjOf a -> StmtMathFragments
+adjMathFragments renderArg (Adj _loc item args) =
+    lexicalItemStmtMathFragments renderArg item args
+
+verbMathFragments :: Bool -> (a -> StmtMathFragments) -> VerbOf a -> StmtMathFragments
+verbMathFragments isPlural renderArg (Verb _loc item args) =
+    lexicalItemSgPlStmtMathFragments isPlural renderArg item args
+
+verbPhraseMathFragments :: HintMap -> Bool -> VerbPhrase -> StmtMathFragments
+verbPhraseMathFragments hints isPlural = \case
+    VPVerb verb ->
+        verbMathFragments isPlural (termMathFragments hints) verb
+    VPAdj adjs ->
+        stmtMathProse (if isPlural then "are " else "is ")
+            <> joinStmtMathFragments (stmtMathProse " and ") (adjMathFragments (termMathFragments hints) <$> toList adjs)
+    VPVerbNot verb ->
+        stmtMathProse (if isPlural then "do not " else "does not ")
+            <> verbMathFragments True (termMathFragments hints) verb
+    VPAdjNot adjs ->
+        stmtMathProse (if isPlural then "are not " else "is not ")
+            <> joinStmtMathFragments (stmtMathProse " and ") (adjMathFragments (termMathFragments hints) <$> toList adjs)
+
+nounMathFragments :: Bool -> (a -> StmtMathFragments) -> NounOf a -> StmtMathFragments
+nounMathFragments isPlural renderArg (Noun _loc item args) =
+    lexicalItemSgPlStmtMathFragments isPlural renderArg item args
+
+funMathFragments :: (a -> StmtMathFragments) -> FunOf a -> StmtMathFragments
+funMathFragments renderArg Fun{phrase, funArgs} =
+    lexicalItemSgPlStmtMathFragments False renderArg phrase funArgs
+
+structPhraseMathFragments :: StructPhrase -> StmtMathFragments
+structPhraseMathFragments item =
+    lexicalItemSgPlStmtMathFragments False termMathPlaceholderFragments item []
+
+termMathPlaceholderFragments :: a -> StmtMathFragments
+termMathPlaceholderFragments _ =
+    stmtMathProse "?"
+
+lexicalItemStmtMathFragments :: (a -> StmtMathFragments) -> LexicalItem -> [a] -> StmtMathFragments
+lexicalItemStmtMathFragments renderArg item args =
+    patternStmtMathFragments renderArg (lexicalItemPhrase item) args
+
+lexicalItemSgPlStmtMathFragments :: Bool -> (a -> StmtMathFragments) -> LexicalItemSgPl -> [a] -> StmtMathFragments
+lexicalItemSgPlStmtMathFragments isPlural renderArg item args =
+    patternStmtMathFragments renderArg phrase args
+    where
+        phrase = if isPlural then pl (lexicalItemSgPlPhrase item) else sg (lexicalItemSgPlPhrase item)
+
+patternStmtMathFragments :: (a -> StmtMathFragments) -> [Maybe Token] -> [a] -> StmtMathFragments
+patternStmtMathFragments renderArg patternParts args =
+    joinStmtMathFragments (stmtMathProse " ") (go patternParts args)
+    where
+        go [] [] = []
+        go [] (_ : _) = error "renderPatternStmtMath: too many arguments"
+        go (Nothing : rest) (arg : restArgs) = renderArg arg : go rest restArgs
+        go (Nothing : _) [] = error "renderPatternStmtMath: not enough arguments"
+        go (Just tok : rest) restArgs = renderStmtToken tok : go rest restArgs
+
+        renderStmtToken :: Token -> StmtMathFragments
+        renderStmtToken = \case
+            Word w -> stmtMathProse w
+            tok -> stmtMathNode (renderMathToken tok)
+
+
+renderFormulaMath :: HintMap -> Formula -> Html ()
+renderFormulaMath hints = \case
+    FormulaChain chain ->
+        renderChainMathRow hints chain
+    FormulaPredicate _loc predi marker exprs ->
+        renderHintedMathRow hints PredicateHint marker (toList exprs) (renderPrefixPredicateFallback predi (renderExprMath hints <$> toList exprs))
+    Connected _loc conn phi psi -> do
+        renderFormulaMath hints phi
+        moText (connectiveSymbol conn)
+        renderFormulaMath hints psi
+    FormulaNeg _loc phi -> do
+        moText "¬"
+        renderFormulaMath hints phi
+    FormulaQuantified _loc quant vars bound phi -> do
+        moText (quantifierSymbol quant)
+        renderVarListMath vars
+        renderBoundMath hints vars bound
+        moText "."
+        renderFormulaMath hints phi
+    PropositionalConstant _loc pc ->
+        moText (propositionalConstantSymbol pc)
+
+connectiveSymbol :: Connective -> Text
+connectiveSymbol = \case
+    Conjunction -> "∧"
+    Disjunction -> "∨"
+    Implication -> "⇒"
+    Equivalence -> "⇔"
+    ExclusiveOr -> "⊕"
+    NegatedDisjunction -> "↓"
+
+quantifierSymbol :: Quantifier -> Text
+quantifierSymbol = \case
+    Universally -> "∀"
+    Existentially -> "∃"
+    Nonexistentially -> "∄"
+
+propositionalConstantSymbol :: PropositionalConstant -> Text
+propositionalConstantSymbol = \case
+    IsBottom -> "⊥"
+    IsTop -> "⊤"
+
+renderChainMathRow :: HintMap -> Chain -> Html ()
+renderChainMathRow hints chain =
+    joinHtml (moText "∧") (renderLink <$> splatChain chain)
+    where
+        renderLink (lhs, sign, rel, rhs) =
+            renderRelationApplication hints sign (toList lhs) rel (toList rhs)
+
+        splatChain :: Chain -> [(NonEmpty Expr, Sign, Relation, NonEmpty Expr)]
+        splatChain = \case
+            ChainBase es sign rel es' ->
+                [(es, sign, rel, es')]
+            ChainCons es sign rel ch'@(ChainBase es' _ _ _) ->
+                (es, sign, rel, es') : splatChain ch'
+            ChainCons es sign rel ch'@(ChainCons es' _ _ _) ->
+                (es, sign, rel, es') : splatChain ch'
+
+renderBoundMath :: HintMap -> NonEmpty VarSymbol -> Bound -> Html ()
+renderBoundMath hints vars = \case
+    Unbounded -> skip
+    Bounded _loc sign rel expr -> do
+        moText ","
+        renderRelationApplication hints sign (ExprVar <$> toList vars) rel [expr]
+
+renderRelationApplication :: HintMap -> Sign -> [Expr] -> Relation -> [Expr] -> Html ()
+renderRelationApplication hints sign lhs rel rhs = case (sign, rel) of
+    (Negative, Relation _loc symbol [])
+        | Just negated <- negatedRelationSymbol (relationSymbolToken symbol) -> do
+            renderExprListMath hints lhs
+            moText negated
+            renderExprListMath hints rhs
+    _ ->
+        applySign sign (renderRelationCore hints lhs rel rhs)
+
+applySign :: Sign -> Html () -> Html ()
+applySign sign html = case sign of
+    Positive -> html
+    Negative -> do
+        mo_ "¬"
+        html
+
+renderRelationCore :: HintMap -> [Expr] -> Relation -> [Expr] -> Html ()
+renderRelationCore hints lhs rel rhs = case rel of
+    Relation _loc symbol relParams -> do
+        renderExprListMath hints lhs
+        renderRelationSymbolCore hints symbol relParams
+        renderExprListMath hints rhs
+    RelationExpr _loc expr -> do
+        renderExprListMath hints lhs
+        renderExprMath hints expr
+        renderExprListMath hints rhs
+
+renderRelationSymbolCore :: HintMap -> RelationSymbol -> [Expr] -> Html ()
+renderRelationSymbolCore hints symbol relParams =
+    renderHintedMathRow
+        hints
+        RelationHint
+        (relationSymbolMarker symbol)
+        relParams
+        (renderRelationFallback hints symbol relParams)
+
+renderRelationFallback :: HintMap -> RelationSymbol -> [Expr] -> Html ()
+renderRelationFallback hints symbol relParams =
+    merror_ (renderRelationFallbackCore hints symbol relParams)
+
+renderRelationFallbackCore :: HintMap -> RelationSymbol -> [Expr] -> Html ()
+renderRelationFallbackCore hints symbol relParams
+    | null relParams = renderRelationToken (relationSymbolToken symbol)
+    | otherwise = msub_ do
+        renderRelationToken (relationSymbolToken symbol)
+        mrow_ (renderExprListMath hints relParams)
+
+renderRelationToken :: Token -> Html ()
+renderRelationToken = \case
+    Command "in" -> moText "∈"
+    Command "ni" -> moText "∋"
+    Command "notin" -> moText "∉"
+    Command "meets" -> moText "⋈"
+    Command "notmeets" -> moText "⋈̸"
+    Command "subset" -> moText "⊂"
+    Command "subseteq" -> moText "⊆"
+    Command "supset" -> moText "⊃"
+    Command "supseteq" -> moText "⊇"
+    Command "neq" -> moText "≠"
+    tok -> renderMathToken tok
+
+negatedRelationSymbol :: Token -> Maybe Text
+negatedRelationSymbol = \case
+    Command "in" -> Just "∉"
+    Command "ni" -> Just "∌"
+    Command "subset" -> Just "⊄"
+    Command "subseteq" -> Just "⊈"
+    Command "supset" -> Just "⊅"
+    Command "supseteq" -> Just "⊉"
+    Command "meets" -> Just "⋈̸"
+    Symbol "=" -> Just "≠"
+    Symbol "<" -> Just "≮"
+    Symbol ">" -> Just "≯"
+    Symbol "≤" -> Just "≰"
+    Symbol "≥" -> Just "≱"
+    _ -> Nothing
+
+
+renderExprMath :: HintMap -> Expr -> Html ()
+renderExprMath hints expr = case expr of
+    ExprVar var ->
+        renderVarMath var
+    ExprInteger _loc n ->
+        mnText (Text.pack (show n))
+    ExprOp _loc item args ->
+        renderHintedMath hints OperatorHint (mixfixMarker item) args (renderPatternFallback (mixfixPattern item) (renderExprMath hints <$> args))
+    ExprStructOp _loc symb maybeExpr ->
+        let marker = structMarker symb
+            args = maybeToList maybeExpr
+        in renderHintedMath hints StructOpHint marker args (renderStructFallback symb (renderExprMath hints <$> args))
+    ExprFiniteSet{} ->
+        mrow_ (renderExprMathRow hints expr)
+    ExprSep{} ->
+        mrow_ (renderExprMathRow hints expr)
+    ExprReplace{} ->
+        mrow_ (renderExprMathRow hints expr)
+    ExprReplacePred{} ->
+        mrow_ (renderExprMathRow hints expr)
+
+renderExprMathRow :: HintMap -> Expr -> Html ()
+renderExprMathRow hints = \case
+    ExprVar var ->
+        renderVarMath var
+    ExprInteger _loc n ->
+        mnText (Text.pack (show n))
+    ExprOp _loc item args ->
+        renderHintedMathRow hints OperatorHint (mixfixMarker item) args (renderPatternFallback (mixfixPattern item) (renderExprMath hints <$> args))
+    ExprStructOp _loc symb maybeExpr ->
+        let marker = structMarker symb
+            args = maybeToList maybeExpr
+        in renderHintedMathRow hints StructOpHint marker args (renderStructFallback symb (renderExprMath hints <$> args))
+    ExprFiniteSet _loc exprs ->
+        renderFiniteSetMath hints (toList exprs)
+    ExprSep _loc var bound stmt -> do
+        moText "{"
+        renderVarMath var
+        moText "∈"
+        renderExprMathRow hints bound
+        moText "|"
+        renderStmtMath hints stmt
+        moText "}"
+    ExprReplace _loc expr bounds maybeStmt -> do
+        moText "{"
+        renderExprMathRow hints expr
+        moText "|"
+        renderReplaceBoundsMath hints (toList bounds)
+        for_ maybeStmt \stmt -> do
+            moText "|"
+            renderStmtMath hints stmt
+        moText "}"
+    ExprReplacePred _loc rangeVar domVar domExpr stmt -> do
+        moText "{"
+        renderVarMath rangeVar
+        moText "|"
+        moText "∃"
+        renderVarMath domVar
+        moText "∈"
+        renderExprMathRow hints domExpr
+        moText "."
+        renderStmtMath hints stmt
+        moText "}"
+
+renderReplaceBoundsMath :: HintMap -> [(VarSymbol, Expr)] -> Html ()
+renderReplaceBoundsMath hints =
+    joinHtml (moText ",") . fmap renderBound
+    where
+        renderBound (var, expr) = do
+            renderVarMath var
+            moText "∈"
+            renderExprMathRow hints expr
+
+renderExprListMath :: HintMap -> [Expr] -> Html ()
+renderExprListMath hints =
+    joinHtml (moText ",") . fmap (renderExprMath hints)
+
+renderFiniteSetMath :: HintMap -> [Expr] -> Html ()
+renderFiniteSetMath hints exprs =
+    do
+        moText "{"
+        renderExprListMath hints exprs
+        moText "}"
+
+renderHintedMath :: HintMap -> HintCategory -> Marker -> [Expr] -> Html () -> Html ()
+renderHintedMath hints category marker args fallback =
+    case Map.lookup (category, marker, length args) hints of
+        Nothing ->
+            fallback
+        Just RenderHint{..}
+            | renderHintArity /= length args ->
+                error ("Render hint arity mismatch for " <> show category <> " " <> show marker <> ": expected " <> show renderHintArity <> ", got " <> show (length args))
+            | otherwise ->
+                renderTemplateAsNode renderHintTemplate
+    where
+        renderedArgs = renderExprMath hints <$> args
+
+        renderTemplateAsNode :: [TemplatePiece] -> Html ()
+        renderTemplateAsNode = \case
+            [piece] ->
+                renderPiece piece
+            pieces ->
+                mrow_ (traverse_ renderPiece pieces)
+
+        renderPiece :: TemplatePiece -> Html ()
+        renderPiece = \case
+            Literal text -> toHtmlRaw text
+            Slot ix -> case nth (ix - 1) renderedArgs of
+                Just html -> html
+                Nothing -> error ("Render hint slot out of bounds for " <> show marker <> ": <x" <> show ix <> "/>")
+
+renderHintedMathRow :: HintMap -> HintCategory -> Marker -> [Expr] -> Html () -> Html ()
+renderHintedMathRow hints category marker args fallback =
+    case Map.lookup (category, marker, length args) hints of
+        Nothing ->
+            fallback
+        Just RenderHint{..}
+            | renderHintArity /= length args ->
+                error ("Render hint arity mismatch for " <> show category <> " " <> show marker <> ": expected " <> show renderHintArity <> ", got " <> show (length args))
+            | otherwise ->
+                traverse_ renderPiece renderHintTemplate
+    where
+        renderedArgs = renderExprMath hints <$> args
+
+        renderPiece :: TemplatePiece -> Html ()
+        renderPiece = \case
+            Literal text -> toHtmlRaw text
+            Slot ix -> case nth (ix - 1) renderedArgs of
+                Just html -> html
+                Nothing -> error ("Render hint slot out of bounds for " <> show marker <> ": <x" <> show ix <> "/>")
+
+renderPatternFallback :: Pattern -> [Html ()] -> Html ()
+renderPatternFallback patternParts renderedArgs =
+    merror_ (renderPatternMath patternParts renderedArgs)
+
+renderPatternMath :: Pattern -> [Html ()] -> Html ()
+renderPatternMath patternParts renderedArgs =
+    traverse_ id (go patternParts renderedArgs)
+    where
+        go End [] = []
+        go End (_ : _) = error "renderPatternMath: too many arguments"
+        go (HoleCons rest) (arg : args) = arg : go rest args
+        go (HoleCons _) [] = error "renderPatternMath: not enough arguments"
+        go (TokenCons tok rest) args = renderMathToken tok : go rest args
+
+renderPrefixPredicateFallback :: PrefixPredicate -> [Html ()] -> Html ()
+renderPrefixPredicateFallback (PrefixPredicate command _arity) renderedArgs =
+        merror_ do
+        miText command
+        when (not (null renderedArgs)) do
+            moText "("
+            joinHtml (moText ",") renderedArgs
+            moText ")"
+
+renderStructFallback :: StructSymbol -> [Html ()] -> Html ()
+renderStructFallback symb renderedArgs =
+    merror_ do
+        renderStructSymbolName symb
+        when (not (null renderedArgs)) do
+            moText "("
+            joinHtml (moText ",") renderedArgs
+            moText ")"
+
+renderStructSymbolName :: StructSymbol -> Html ()
+renderStructSymbolName (StructSymbol name) = miText name
+
+structMarker :: StructSymbol -> Marker
+structMarker (StructSymbol name) = Marker name
+
+renderMathToken :: Token -> Html ()
+renderMathToken = \case
+    Word w -> miText w
+    Variable v -> renderNamedVariableMath v
+    Symbol s -> moText s
+    Integer n -> mnText (Text.pack (show n))
+    Command cmd -> miText cmd
+    Label m -> mtextText ("label:" <> m)
+    Ref ms -> mtextText ("ref:" <> Text.intercalate "," (toList ms))
+    BeginEnv env -> mtextText ("begin:" <> env)
+    EndEnv env -> mtextText ("end:" <> env)
+    ParenL -> moText "("
+    ParenR -> moText ")"
+    BracketL -> moText "["
+    BracketR -> moText "]"
+    VisibleBraceL -> moText "{"
+    VisibleBraceR -> moText "}"
+    InvisibleBraceL -> moText "("
+    InvisibleBraceR -> moText ")"
+
+
+inlineMath :: Html () -> Html ()
+inlineMath inner = math_ inner
+
+blockMath :: Html () -> Html ()
+blockMath inner = math_ [displayblock_] inner
+
+renderVarInline :: VarSymbol -> Html ()
+renderVarInline = inlineMath . renderVarMath
+
+renderVarMath :: VarSymbol -> Html ()
+renderVarMath = \case
+    NamedVarAt _loc name ->
+        renderNamedVariableMath name
+    FreshVarAt _loc n ->
+        miText ("_" <> Text.pack (show n))
+
+renderNamedVariableMath :: Text -> Html ()
+renderNamedVariableMath rawName =
+    case displayVariable rawName of
+        VariableDisplay baseText Nothing ->
+            miText baseText
+        VariableDisplay baseText (Just (VariableTicks tickCount)) ->
+            msup_ do
+                miText baseText
+                renderPrimeSuperscript tickCount
+        VariableDisplay baseText (Just (VariableSubscript subscriptText)) ->
+            msub_ do
+                miText baseText
+                renderVariableSubscriptMath subscriptText
+
+renderPrimeSuperscript :: Int -> Html ()
+renderPrimeSuperscript tickCount
+    | tickCount <= 1 =
+        moText "′"
+    | otherwise =
+        mrow_ (foldMap (const (moText "′")) [1 .. tickCount])
+
+renderVariableSubscriptMath :: Text -> Html ()
+renderVariableSubscriptMath subscriptText
+    | Text.all isDigit subscriptText =
+        mnText subscriptText
+    | otherwise =
+        miText subscriptText
+
+renderVarEqInline :: HintMap -> VarSymbol -> Expr -> Html ()
+renderVarEqInline hints var expr =
+    inlineMath do
+        renderVarMath var
+        moText "="
+        renderExprMathRow hints expr
+
+renderFunctionCallInline :: VarSymbol -> VarSymbol -> Html ()
+renderFunctionCallInline fun arg =
+    inlineMath (renderFunctionCallMath fun arg)
+
+renderFunctionEqInline :: HintMap -> VarSymbol -> VarSymbol -> Expr -> Html ()
+renderFunctionEqInline hints fun arg expr =
+    inlineMath do
+        renderFunctionCallMath fun arg
+        moText "="
+        renderExprMathRow hints expr
+
+renderFunctionCallMath :: VarSymbol -> VarSymbol -> Html ()
+renderFunctionCallMath fun arg = do
+    renderVarMath fun
+    moText "("
+    renderVarMath arg
+    moText ")"
+
+renderVarListInline :: NonEmpty VarSymbol -> Html ()
+renderVarListInline vars =
+    inlineMath (renderVarListMath vars)
+
+renderVarListMath :: NonEmpty VarSymbol -> Html ()
+renderVarListMath vars =
+    joinHtml (moText ",") (renderVarMath <$> toList vars)
+
+renderBoundInline :: HintMap -> NonEmpty VarSymbol -> Bound -> Html ()
+renderBoundInline hints vars = \case
+    Unbounded -> skip
+    bound -> do
+        toHtml (" with " :: Text)
+        inlineMath (renderBoundPhraseMath hints vars bound)
+
+renderBoundSubjectInline :: HintMap -> NonEmpty VarSymbol -> Bound -> Html ()
+renderBoundSubjectInline hints vars = \case
+    Unbounded ->
+        renderVarListInline vars
+    bound ->
+        inlineMath (renderBoundSubjectMath hints vars bound)
+
+renderBoundPhraseMath :: HintMap -> NonEmpty VarSymbol -> Bound -> Html ()
+renderBoundPhraseMath hints vars = \case
+    Unbounded -> mrow_ skip
+    Bounded _loc sign rel expr ->
+        renderRelationApplication hints sign (ExprVar <$> toList vars) rel [expr]
+
+renderBoundSubjectMath :: HintMap -> NonEmpty VarSymbol -> Bound -> Html ()
+renderBoundSubjectMath hints vars = \case
+    Unbounded ->
+        renderVarListMath vars
+    Bounded _loc sign rel expr ->
+        renderRelationApplication hints sign (ExprVar <$> toList vars) rel [expr]
+
+boundSubjectMathFragments :: HintMap -> NonEmpty VarSymbol -> Bound -> StmtMathFragments
+boundSubjectMathFragments hints vars = \case
+    Unbounded ->
+        stmtMathNode (renderVarListMath vars)
+    bound ->
+        stmtMathNode (renderBoundSubjectMath hints vars bound)
+
+renderSymbolPatternInline :: HintMap -> SymbolPattern -> Html ()
+renderSymbolPatternInline hints =
+    inlineMath . renderSymbolPatternMath hints
+
+renderSymbolPatternMath :: HintMap -> SymbolPattern -> Html ()
+renderSymbolPatternMath hints (SymbolPattern symbol vars) =
+    renderHintedMathRow hints OperatorHint (mixfixMarker symbol) (ExprVar <$> vars) (renderPatternFallback (mixfixPattern symbol) (renderVarMath <$> vars))
+
+renderJustification :: ReferenceContext -> Justification -> Html ()
+renderJustification references = \case
+    JustificationRef markers -> do
+        toHtml ("by " :: Text)
+        renderMarkerReferences references (toList markers)
+    JustificationSetExt ->
+        toHtml ("by set extensionality" :: Text)
+    JustificationEmpty ->
+        skip
+    JustificationLocal ->
+        toHtml ("by local assumptions" :: Text)
+
+renderJustificationSuffix :: ReferenceContext -> Justification -> Html ()
+renderJustificationSuffix _ JustificationEmpty = skip
+renderJustificationSuffix references justification = do
+    toHtml (" " :: Text)
+    renderJustification references justification
+
+renderMarkerReferences :: ReferenceContext -> [Marker] -> Html ()
+renderMarkerReferences references markers
+    | length markers >= referenceGroupThreshold =
+        renderMarkerReferenceGroup references markers
+    | otherwise =
+        joinHtml (toHtml (", " :: Text)) (renderMarkerReference references <$> markers)
+
+renderMarkerReferenceGroup :: ReferenceContext -> [Marker] -> Html ()
+renderMarkerReferenceGroup references markers =
+    span_ groupAttributes do
+        toHtml ("[...]" :: Text)
+        span_ [class_ "reference-preview-group-items", makeAttributes "hidden" "hidden"] do
+            traverse_ (renderMarkerReferenceGroupItem references) markers
+    where
+        referenceCountLabel = Text.pack (show (length markers)) <> " references"
+
+        groupAttributes =
+            [ class_ "ref-badge has-preview ref-badge-group"
+            , makeAttributes "data-preview-group" "true"
+            , makeAttributes "data-reference-label" referenceCountLabel
+            , makeAttributes "aria-describedby" "reference-preview-popup"
+            , makeAttributes "tabindex" "0"
+            , makeAttributes "role" "button"
+            , makeAttributes "aria-label" ("Show " <> referenceCountLabel)
+            ]
+
+renderMarkerReferenceGroupItem :: ReferenceContext -> Marker -> Html ()
+renderMarkerReferenceGroupItem ReferenceContext{..} marker =
+    span_ itemAttributes skip
+    where
+        label = markerText marker
+        baseAttributes =
+            [ class_ "reference-preview-group-item"
+            , makeAttributes "data-reference-label" label
+            ]
+
+        itemAttributes =
+            baseAttributes <> case Map.lookup marker referenceAnchors of
+                Just anchor ->
+                    [ makeAttributes
+                        "data-preview-link"
+                        (renderUrlFragment anchor)
+                    , makeAttributes "data-preview-target-id" anchor
+                    ]
+                Nothing ->
+                    case Map.lookup marker referencePreviews of
+                        Nothing ->
+                            []
+                        Just preview ->
+                            [ makeAttributes
+                                "data-preview-link"
+                                (previewReferenceHref preview)
+                            , makeAttributes "data-preview-id" (previewId preview)
+                            ]
+
+renderMarkerReference :: ReferenceContext -> Marker -> Html ()
+renderMarkerReference ReferenceContext{..} marker =
+    case Map.lookup marker referenceAnchors of
+        Just anchor ->
+            a_
+                ( href_ (renderUrlFragment anchor)
+                    : referenceAttributes
+                        (Just (currentPreviewAttributes anchor))
+                )
+                (toHtml label)
+        Nothing ->
+            case Map.lookup marker referencePreviews of
+                Nothing ->
+                    span_ (referenceAttributes Nothing) (toHtml label)
+                Just preview ->
+                    a_
+                        ( href_ (previewReferenceHref preview)
+                        : referenceAttributes (Just (importedPreviewAttributes preview))
+                        )
+                        (toHtml label)
+    where
+        label = markerText marker
+
+        referenceAttributes preview =
+            [ class_ (if hasPreview preview then "ref-badge has-preview" else "ref-badge")
+            , makeAttributes "data-reference-label" label
+            ]
+            <> foldMap id preview
+
+        hasPreview =
+            \case
+                Nothing -> False
+                Just _ -> True
+
+        currentPreviewAttributes anchor =
+            [ makeAttributes "data-preview-target-id" anchor
+            , makeAttributes "aria-describedby" "reference-preview-popup"
+            ]
+
+        importedPreviewAttributes entry =
+            [ makeAttributes "data-preview-id" (previewId entry)
+            , makeAttributes "aria-describedby" "reference-preview-popup"
+            ]
+
+
+markerText :: Marker -> Text
+markerText (Marker text) = text
+
+tokenTextHtml :: Token -> Html ()
+tokenTextHtml = toHtml . tokToText
+
+joinHtml :: Html () -> [Html ()] -> Html ()
+joinHtml _ [] = mempty
+joinHtml separator (x : xs) = x <> foldMap (separator <>) xs
+
+miText :: Text -> Html ()
+miText = mi_ . toHtml
+
+moText :: Text -> Html ()
+moText = mo_ . toHtml
+
+mnText :: Text -> Html ()
+mnText = mn_ . toHtml
+
+mtextText :: Text -> Html ()
+mtextText = mtext_ . toHtml