:root {
  --bg: #ffffff; --fg: #1a1a1a; --dim: #6a6a6a; --line: #e0e0e0; --card: #fafafa; --code: #f3f3f3;
  --ok: #1a7f37; --warn: #9a6700; --bad: #b42318; --link: #0b57d0;
  --k-theorem: #0b57d0; --k-def: #6f42c1; --k-inductive: #1a7f37; --k-constructor: #2a9d8f; --k-recursor: #8a8a8a;
  --k-axiom: #b42318; --k-opaque: #b26a00; --k-quot: #8a8a8a; --k-unknown: #8a8a8a;
}
/* The operating system decides unless the reader says otherwise; data-theme is that override, and it has to
   beat the media query, so the media query steps aside when it is present. */
@media (prefers-color-scheme: dark) {
  :root:not([data-theme]) {
    --bg: #16181a; --fg: #e6e6e6; --dim: #9aa0a6; --line: #2c3033; --card: #1c1f21; --code: #22262a;
    --ok: #4ac26b; --warn: #d4a72c; --bad: #ff7b72; --link: #7aa7ff;
    --k-theorem: #7aa7ff; --k-def: #c49bff; --k-inductive: #4ac26b; --k-constructor: #5fd3c4; --k-recursor: #9aa0a6;
    --k-axiom: #ff7b72; --k-opaque: #e0a34a;
  }
}
:root[data-theme="dark"] {
    --bg: #16181a; --fg: #e6e6e6; --dim: #9aa0a6; --line: #2c3033; --card: #1c1f21; --code: #22262a;
    --ok: #4ac26b; --warn: #d4a72c; --bad: #ff7b72; --link: #7aa7ff;
    --k-theorem: #7aa7ff; --k-def: #c49bff; --k-inductive: #4ac26b; --k-constructor: #5fd3c4; --k-recursor: #9aa0a6;
    --k-axiom: #ff7b72; --k-opaque: #e0a34a;
}
/* The browser's own `[hidden] { display: none }` loses to any author rule that sets display, which is how a
   palette with `display: flex` came to cover every page and how the chomp row stayed painted while marked
   hidden. Stating it once, loudly, removes the whole category rather than the two instances we happened to
   notice. Anything that wants to be hidden and still laid out should not be using the attribute. */
[hidden] { display: none !important; }

* { box-sizing: border-box; }
html { background: var(--bg); }
body { margin: 0; background: var(--bg); color: var(--fg);
       font: 15px/1.55 ui-sans-serif, -apple-system, "Segoe UI", system-ui, sans-serif; }
a { color: var(--link); text-decoration: none; }
a:hover { text-decoration: underline; }
code, pre, .nm, .mono { font-family: ui-monospace, "SF Mono", Menlo, Consolas, monospace; font-size: 13px; }
header { display: flex; flex-direction: column; gap: 8px; padding: 10px 16px; border-bottom: 1px solid var(--line);
         position: sticky; top: 0; background: var(--bg); z-index: 5; }
/* Two rows: what you do (search, map) above what you are looking at (library, filter). One row held a brand,
   a search field, five library pills, a long checkbox label and a status line, and read as a pile. */
header .bar { display: flex; gap: 16px; align-items: center; flex-wrap: wrap; }
header .bar.sub { gap: 12px; font-size: 13px; }
header .bar.sub .switch { color: var(--dim); }
header .bar.sub #scopewrap { margin-left: auto; }
header .bar.sub #scopewrap[hidden] + .switch { margin-left: auto; }
.maplink { display: inline-flex; align-items: center; gap: 7px; padding: 5px 11px; border: 1px solid var(--line);
           border-radius: 8px; color: var(--fg); font-size: 13px; white-space: nowrap; }
.maplink:hover { border-color: var(--link); text-decoration: none; }
.maplink.on { border-color: var(--link); background: var(--code); }
.mapicon { width: 22px; height: 16px; display: block; }
/* the treemap's own palette, so the icon reads as a small picture of the page it opens */
.mapicon rect { stroke: var(--line); stroke-width: 1; }
.mapicon rect:nth-child(1) { fill: hsl(280 45% 45% / .55); }
.mapicon rect:nth-child(2) { fill: hsl(0 45% 45% / .55); }
.mapicon rect:nth-child(3) { fill: hsl(170 45% 45% / .55); }
.mapicon rect:nth-child(4) { fill: hsl(280 45% 45% / .4); }
.mapicon rect:nth-child(5) { fill: hsl(220 45% 45% / .55); }
.brand { font-weight: 700; color: var(--fg); white-space: nowrap; }
.search { position: relative; flex: 1; max-width: 640px; }
.search input { width: 100%; padding: 8px 12px; border: 1px solid var(--line); border-radius: 8px;
                background: var(--card); color: var(--fg); font: inherit; }
.results { position: absolute; left: 0; right: 0; top: 40px; background: var(--bg); border: 1px solid var(--line);
           border-radius: 8px; box-shadow: 0 8px 24px rgba(0,0,0,.12); max-height: 60vh; overflow: auto; }
.results a { display: flex; gap: 10px; padding: 6px 12px; color: var(--fg); align-items: baseline; }
.results a:hover, .results a.active { background: var(--code); text-decoration: none; }
.results .mod { margin-left: auto; }
.status { color: var(--dim); font-size: 12px; white-space: nowrap; }
main { max-width: 1180px; margin: 0 auto; padding: 24px 16px 64px; }
footer { max-width: 1180px; margin: 0 auto; padding: 16px; border-top: 1px solid var(--line); color: var(--dim); font-size: 12px; }
h1 { font-size: 20px; margin: 0 0 6px; font-family: ui-monospace, "SF Mono", Menlo, monospace; font-weight: 600; word-break: break-word; overflow-wrap: anywhere; }
h1.prose { font-family: inherit; word-break: normal; overflow-wrap: normal; }
h1 .ns { color: var(--dim); font-weight: 500; }
h2 { font-size: 12px; text-transform: uppercase; letter-spacing: .08em; color: var(--dim); margin: 28px 0 10px; font-weight: 600; }
h2 small { text-transform: none; letter-spacing: 0; font-weight: 400; }
.dim { color: var(--dim); }
.sub { color: var(--dim); font-size: 13px; margin: 0 0 14px; display: flex; gap: 14px; flex-wrap: wrap; align-items: center; }
.kind { display: inline-block; font-size: 11px; font-weight: 600; letter-spacing: .04em; text-transform: uppercase;
        padding: 1px 6px; border-radius: 4px; border: 1px solid currentColor; line-height: 1.5; }
.kind.theorem { color: var(--k-theorem); } .kind.def { color: var(--k-def); } .kind.inductive { color: var(--k-inductive); }
.kind.constructor { color: var(--k-constructor); } .kind.recursor { color: var(--k-recursor); } .kind.axiom { color: var(--k-axiom); }
.kind.opaque { color: var(--k-opaque); } .kind.quot, .kind.unknown { color: var(--k-quot); }
.verdict { display: inline-block; padding: 3px 10px; border-radius: 999px; font-size: 13px; font-weight: 600; border: 1px solid currentColor; }
.verdict.ok { color: var(--ok); } .verdict.warn { color: var(--warn); } .verdict.bad { color: var(--bad); }
pre { background: var(--code); border: 1px solid var(--line); border-radius: 6px; padding: 12px 14px; overflow-x: auto;
      white-space: pre-wrap; word-break: break-word; margin: 0; }
pre a { color: var(--link); }
.doc { max-width: 78ch; }
.doc p { margin: 0 0 10px; }
.doc code { background: var(--code); padding: 1px 4px; border-radius: 3px; }
.doc pre { margin: 0 0 10px; }
.cols { display: grid; grid-template-columns: 1fr 1fr; gap: 24px; }
@media (max-width: 800px) { .cols { grid-template-columns: 1fr; } }
.list { list-style: none; margin: 0; padding: 0; }
.list li { display: flex; gap: 8px; align-items: baseline; padding: 3px 0; border-bottom: 1px solid var(--line); flex-wrap: wrap; }
.list .nm { word-break: break-all; }
.list .mod, .mod { color: var(--dim); font-size: 12px; }
.list .n { margin-left: auto; color: var(--dim); font-size: 12px; font-variant-numeric: tabular-nums; }
.stats { display: flex; flex-wrap: wrap; gap: 24px; margin: 0; padding: 0; list-style: none; }
.stats div { font-size: 12px; color: var(--dim); }
.stats b { display: block; font-size: 20px; color: var(--fg); font-weight: 600; font-variant-numeric: tabular-nums; }
.card { background: var(--card); border: 1px solid var(--line); border-radius: 8px; padding: 14px 16px; margin-bottom: 12px; }
.graph { width: 100%; height: auto; display: block; border: 1px solid var(--line); border-radius: 8px; background: var(--card); }
.graph .edge { fill: none; stroke: var(--line); stroke-width: 1.2; }
.graph .edge.stmt { stroke: var(--k-theorem); opacity: .55; }
.graph .node rect { fill: var(--bg); stroke: var(--line); rx: 5; }
.graph .node text { font: 12px ui-monospace, "SF Mono", Menlo, monospace; fill: var(--fg); }
.graph .node.center rect { stroke: var(--fg); stroke-width: 1.5; }
.graph .node:hover rect { stroke: var(--link); }
.graph .lbl { font: 11px ui-sans-serif, system-ui, sans-serif; fill: var(--dim); text-transform: uppercase; letter-spacing: .08em; }
.graph .swatch { stroke-width: 3; }
.tree ul { list-style: none; margin: 0; padding-left: 18px; }
.tree > ul { padding-left: 0; }
.tree li { padding: 2px 0; }
.tree .tog { cursor: pointer; user-select: none; display: inline-block; width: 16px; color: var(--dim); }
.tree .cnt { color: var(--dim); font-size: 12px; margin-left: 6px; font-variant-numeric: tabular-nums; }
.start a { margin-right: 14px; }
.stmt-line { color: var(--dim); font-size: 12px; overflow: hidden; text-overflow: ellipsis; white-space: nowrap; max-width: 60ch; }
button.more { background: none; border: 1px solid var(--line); color: var(--link); border-radius: 6px; padding: 4px 10px; cursor: pointer; font: inherit; font-size: 13px; }
.bad-card { border-color: var(--bad); }
.bad-card code { word-break: break-word; }
.graph .node.far rect { stroke-dasharray: 3 2; }
.graph .edge.far { stroke-dasharray: 3 3; }
.graph-scroll { overflow-x: auto; border: 1px solid var(--line); border-radius: 8px; }
.graph-scroll .graph { border: 0; border-radius: 0; }
.switch { display: flex; gap: 6px; align-items: center; cursor: pointer; }
.switch input { margin: 0; }
.roles { margin: 6px 0 18px; }
.tabs { display: flex; flex-wrap: wrap; gap: 8px; }
.tab { background: var(--card); border: 1px solid var(--line); color: var(--fg); border-radius: 999px; padding: 6px 14px; cursor: pointer; font: inherit; font-size: 14px; }
.tab:hover { border-color: var(--link); }
.tab.on { background: var(--fg); color: var(--bg); border-color: var(--fg); }
.role-body { background: var(--card); border: 1px solid var(--line); border-radius: 10px; padding: 6px 18px 14px; margin-top: 12px; max-width: 86ch; }
.role-body h3 { font-size: 15px; margin: 14px 0 6px; }
.role-body p, .role-body li { max-width: 80ch; }
.role-body ul { padding-left: 20px; }
.role-body li { margin: 4px 0; }
.role-body pre { margin: 8px 0; }
.tour { padding-left: 22px; }
.tour li { margin: 6px 0; }
.gloss { display: grid; grid-template-columns: max-content 1fr; gap: 4px 14px; margin: 0; }
.gloss dt { font-family: ui-monospace, "SF Mono", Menlo, monospace; font-size: 13px; color: var(--k-theorem); }
.gloss dd { margin: 0; }
.explain { margin: 14px 0 0; border: 1px solid var(--line); border-radius: 8px; padding: 8px 14px; background: var(--card); max-width: 86ch; }
.explain summary { cursor: pointer; color: var(--link); font-size: 14px; }
.explain p { margin: 8px 0 4px; font-size: 14px; }
/* Six libraries in a row of pills is 590px, which is wider than a phone. They wrap now. */
.projects { display: flex; gap: 4px; flex-wrap: wrap; }
.projects .proj { padding: 4px 10px; border-radius: 999px; border: 1px solid var(--line); color: var(--fg); font-size: 13px; white-space: nowrap; }
.projects .proj:hover { border-color: var(--link); text-decoration: none; }
.projects .proj.on { background: var(--fg); color: var(--bg); border-color: var(--fg); }
.list li a.kbd, .results a.kbd { outline: 2px solid var(--link); outline-offset: 2px; border-radius: 4px; }
button.cite { margin-left: 8px; }
#keys { position: fixed; inset: 0; background: rgba(0,0,0,.45); display: flex; align-items: center; justify-content: center; z-index: 20; }
.keys-card { background: var(--bg); border: 1px solid var(--line); border-radius: 10px; padding: 18px 24px; min-width: 300px; }
.keys-card h3 { margin: 0 0 10px; font-size: 14px; }
.keys-card .gloss dt { color: var(--fg); }
.treemap { width: 100%; height: auto; background: var(--card); border: 1px solid var(--line); border-radius: 8px; }
.treemap text { font: 13px ui-sans-serif, system-ui, sans-serif; fill: var(--fg); }
.treemap text.n { font-size: 11px; fill: var(--dim); font-variant-numeric: tabular-nums; }
.treemap a:hover rect { stroke: var(--link); stroke-width: 2; }
.prefix { width: 100%; max-width: 420px; padding: 6px 10px; border: 1px solid var(--line); border-radius: 6px; background: var(--card); color: var(--fg); font: inherit; font-size: 13px; }
.dep-card { border-color: var(--warn); }
.nm.dep { text-decoration: line-through; text-decoration-color: var(--warn); }
.depmark { font-size: 11px; color: var(--warn); border: 1px solid currentColor; border-radius: 4px; padding: 0 4px; }
.s-kw { color: var(--k-def); }
.s-op { color: var(--dim); }
.s-rel { color: var(--k-inductive); }
.s-big { color: var(--k-opaque); }
.s-sort { color: var(--k-recursor); }
h1 a.ns { color: var(--dim); font-weight: 500; }
h1 a.ns:hover { color: var(--link); text-decoration: none; }
.tex { font-family: ui-serif, Georgia, "Times New Roman", serif; font-style: italic; }
.tex sub, .tex sup { font-size: .75em; font-style: normal; }
.tex-rm { font-style: normal; font-family: inherit; }
.tex-frac { display: inline-flex; flex-direction: column; vertical-align: -0.45em; text-align: center; font-size: .85em; }
.tex-frac > span:first-child { border-bottom: 1px solid currentColor; padding: 0 .25em; }
.theorem { background: var(--code); border: 1px solid var(--line); border-radius: 6px; padding: 12px 14px; }
.theorem .row { display: flex; gap: 12px; align-items: baseline; padding: 3px 0; }
.theorem .row + .row { border-top: 1px solid var(--line); margin-top: 3px; padding-top: 7px; }
.theorem .lead { flex: 0 0 4.5em; text-align: right; color: var(--dim); font-size: 12px; font-style: italic; }
.theorem .terms { flex: 1; min-width: 0; font-family: ui-monospace, "SF Mono", Menlo, monospace; font-size: 13px; }
.theorem .terms > div { padding: 1px 0; overflow-wrap: anywhere; }
.theorem .hn { color: var(--dim); font-size: 12px; }
.theorem .claim .terms { font-weight: 600; }
.theorem .asone { margin-top: 8px; }
.theorem .asone summary { color: var(--dim); font-size: 12px; cursor: pointer; }
.theorem .asone pre { margin-top: 6px; background: var(--bg); }
.chomp { display: flex; align-items: center; gap: 10px; font-family: ui-monospace, "SF Mono", Menlo, monospace;
         font-size: 13px; color: var(--dim); background: var(--card); border: 1px solid var(--line);
         border-radius: 6px; padding: 8px 12px; margin: 14px 0; min-height: 34px; overflow: hidden; }
.chomp .mouth { color: var(--k-opaque); font-size: 17px; line-height: 1; transform: rotate(-20deg); }
.chomp .mouth.open { transform: rotate(0deg); }
.chomp .crumbs { flex: 1; white-space: nowrap; overflow: hidden; color: var(--fg); opacity: .55; }
.chomp .ate { font-variant-numeric: tabular-nums; }
@media (prefers-reduced-motion: reduce) { .chomp { display: none; } }

/* the line you paste at the top of a file: a Lean user's first question about any declaration */
.importline { margin: 10px 0 14px; display: flex; align-items: center; gap: 8px; flex-wrap: wrap; }
.importline code { background: var(--code); padding: 4px 9px; border-radius: 6px; font-size: 13px; }
button.copy { font-size: 12px; }

/* the treemap's tooltip, and the pooled box for parts too small to draw */
.mapwrap { position: relative; }
.maptip { position: absolute; pointer-events: none; background: var(--bg); border: 1px solid var(--line);
          border-radius: 6px; padding: 6px 10px; font-size: 12px; box-shadow: 0 6px 20px rgba(0,0,0,.35);
          max-width: 420px; z-index: 3; }
.maptip b { display: block; font-family: ui-monospace, "SF Mono", Menlo, monospace; font-weight: 600; }
.maptip span { color: var(--dim); }
.treemap rect.pool { fill: var(--code); stroke: var(--line); stroke-dasharray: 3 3; }
.treemap rect.leaf { stroke-dasharray: none; }

/* what a structure is made of, and the modifiers a reader acts on */
table.fields { border-collapse: collapse; width: 100%; margin: 6px 0 4px; }
table.fields td { padding: 4px 10px 4px 0; vertical-align: top; border-top: 1px solid var(--line); font-size: 13px; }
table.fields td.fname { font-family: ui-monospace, "SF Mono", Menlo, monospace; color: var(--fg); white-space: nowrap; }
.mark { font-size: 11px; border: 1px solid currentColor; border-radius: 4px; padding: 0 5px; color: var(--dim); }
.mark.unsafe, .mark.partial { color: var(--warn); }

.copies { display: flex; gap: 6px; flex-wrap: wrap; margin: 0 0 14px; }
button.why { margin-left: auto; font-size: 11px; }
.chain { line-height: 2; word-break: break-word; }

pre.minimports { margin: 4px 0 8px; }

a.metric { font-size: 12px; padding: 1px 7px; border: 1px solid var(--line); border-radius: 999px; color: var(--dim); }
a.metric.on { color: var(--fg); border-color: var(--link); }
a.metric:hover { text-decoration: none; border-color: var(--link); }

.srcwrap pre { margin: 8px 0 0; max-height: 460px; overflow: auto; }

/* one key to reach anything */
#palette { position: fixed; inset: 0; background: rgba(0,0,0,.45); display: flex; justify-content: center;
           align-items: flex-start; padding-top: 12vh; z-index: 30; }
.pal-card { background: var(--bg); border: 1px solid var(--line); border-radius: 10px; width: min(560px, 92vw);
            box-shadow: 0 16px 48px rgba(0,0,0,.4); overflow: hidden; }
#pal-q { width: 100%; padding: 12px 14px; border: 0; border-bottom: 1px solid var(--line);
         background: var(--bg); color: var(--fg); font: inherit; outline: none; }
#pal-list { max-height: 50vh; overflow: auto; }
#pal-list a { display: flex; gap: 10px; padding: 7px 14px; color: var(--fg); align-items: baseline; }
#pal-list a .mod { margin-left: auto; }
#pal-list a.active, #pal-list a:hover { background: var(--code); text-decoration: none; }

/* Nothing may push the page sideways. A long name, a code span or a wide row scrolls inside its own box
   instead, because a page that scrolls horizontally is one where the reader loses the left margin and every
   line starts somewhere different. */
body { overflow-x: hidden; }
code, .mono, .nm { overflow-wrap: anywhere; }
p.start { display: flex; flex-wrap: wrap; gap: 6px; align-items: baseline; }
@media (max-width: 620px) {
  header { padding: 8px 12px; }
  header .bar { gap: 8px; }
  main { padding: 16px 12px 48px; }
  .search { flex-basis: 100%; order: 3; max-width: none; }
  .cols { grid-template-columns: 1fr; }
  table.fields td { display: block; padding-right: 0; }
  table.fields td.fname { padding-top: 8px; border-top: 1px solid var(--line); }
  table.fields td:last-child { border-top: 0; padding-bottom: 8px; }
}