/* Reading theme. Loaded after Verso's defaults; follows the OS without JavaScript.
   Light: "Light Warm" — sepia paper, warm brown ink, brick-red keywords.
   Dark: the edsulaiman/jetbrains-rider-dark-theme VS Code clone of Rider —
   #262626 editor ground, blue keywords, purple types, tan strings.
   Every text colour below has at least 4.5:1 contrast against the
   background it sits on. */
:root {
  color-scheme: light dark;
  --verso-text-font-family: "Iowan Old Style", "Palatino Linotype", "Book Antiqua", Palatino, Georgia, serif;
  --verso-structure-font-family: system-ui, -apple-system, "Segoe UI", sans-serif;
  --verso-code-font-family: "JetBrains Mono", "DejaVu Sans Mono", "SFMono-Regular", Consolas, "Liberation Mono", monospace;

  /* Light Warm: page and surfaces */
  --verso-background-color: #f7f0df;
  --verso-surface-color: #efe5cf;
  --verso-text-color: #3a3226;
  --verso-structure-color: #2e2820;
  --verso-muted-color: #6e6250;
  --verso-border-color: #d9cbae;
  --verso-link-color: #1d5c73;
  --verso-link-visited-color: #70375f;
  --verso-link-hover-bg: #efe0bc;
  --verso-current-bg: #e6d3a7;
  --verso-current-fg: #3a3226;
  --verso-breadcrumb-color: var(--verso-muted-color);

  /* Light Warm: code */
  --verso-code-box-background-color: #fdf9ee;
  --verso-code-box-border-color: #d9cbae;
  --verso-code-color: #3d352a;
  --verso-code-keyword-color: #9e2b1e;
  --verso-code-keyword-weight: normal;
  --verso-code-const-color: #1f5c7a;
  --verso-code-const-weight: normal;
  --verso-code-var-color: #7a3b6e;
  --verso-code-var-style: italic;
  --verso-code-ctor-color: #14705e;
  --verso-code-def-color: #8a4b0e;
  --verso-code-string-color: #406b2e;
  --verso-code-number-color: #8a5a00;
  --verso-code-comment-color: #71644e;
  --verso-code-doc-color: #5f7355;
  --verso-code-punct-color: #7a6e58;
  --verso-code-annotation-color: #6b6210;
  --verso-code-hover-bg-color: #f0e2c4;
  --verso-inline-code-bg: #efe5cc;
  --verso-selected-color: #f0dfae;

  /* Light Warm: tooltips, proof states, diagnostics */
  --verso-tooltip-color: var(--verso-code-color);
  --verso-tooltip-bg-color: #fffbef;
  --verso-tooltip-border-color: #b3a586;
  --verso-tooltip-separator-color: var(--verso-border-color);
  --verso-tactic-state-color: var(--verso-code-color);
  --verso-tactic-state-bg-color: var(--verso-tooltip-bg-color);
  --verso-tactic-state-border-color: var(--verso-tooltip-border-color);
  --verso-tactic-toggle-color: #a79b80;
  --verso-tactic-toggle-checked-color: #1d5c73;
  --verso-info-indicator-color: #1f5c7a;
  --verso-code-info-hover-bg-color: #dce8ec;
  --verso-tooltip-info-border-color: #a9c4cf;
  --verso-message-info-color: var(--verso-tooltip-color);
  --verso-output-info-color: var(--verso-info-indicator-color);
  --verso-warning-indicator-color: #8a5a00;
  --verso-code-warning-hover-bg-color: #f5e3b0;
  --verso-tooltip-warning-border-color: #d9b96a;
  --verso-message-warning-color: #7a5200;
  --verso-output-warning-color: var(--verso-warning-indicator-color);
  --verso-error-indicator-color: #b3261e;
  --verso-code-error-hover-bg-color: #f3d3ce;
  --verso-tooltip-error-border-color: #d8a09a;
  --verso-message-error-color: #9e2b1e;
  --verso-output-error-color: var(--verso-error-indicator-color);

  /* Light Warm: remaining chrome */
  --verso-imports-summary-color: var(--verso-muted-color);
  --verso-output-color: var(--verso-code-color);
  --verso-blockquote-color: #5e5342;
  --verso-blockquote-border-color: #cbbd97;
  --verso-docstring-border-color: var(--verso-border-color);
  --verso-copy-button-bg: var(--verso-surface-color);
  --verso-copy-button-color: var(--verso-muted-color);
  --verso-copy-button-border: var(--verso-border-color);
  --verso-copy-button-hover-bg: var(--verso-code-hover-bg-color);
  --verso-copy-button-copied-color: #406b2e;
  --verso-hamburger-bg: var(--verso-surface-color);
  --verso-hamburger-border: var(--verso-border-color);
  --verso-hamburger-bar-color: var(--verso-text-color);
}

@media (prefers-color-scheme: dark) {
  :root {
    /* Rider dark, following the edsulaiman/jetbrains-rider-dark-theme VS Code
       clone: chrome #1E1F22 / #2B2D30, editor ground #262626, text #BDBDBD. */
    --verso-background-color: #1e1f22;
    --verso-surface-color: #2b2d30;
    --verso-text-color: #bdbdbd;
    --verso-structure-color: #dfe1e5;
    --verso-muted-color: #9fa1a5;
    --verso-border-color: #393b41;
    --verso-link-color: #82acfc;
    --verso-link-visited-color: #c191ff;
    --verso-link-hover-bg: #2e436e;
    --verso-current-bg: #2e436e;
    --verso-current-fg: #ffffff;
    --verso-breadcrumb-color: var(--verso-muted-color);

    /* Clone syntax colours on the #262626 editor ground. Verso has a single
       `const` class for types and functions, so it takes the clone's type
       purple; locals keep the clone's plain foreground and stay distinct
       through italics. */
    --verso-code-box-background-color: #262626;
    --verso-code-box-border-color: #393b41;
    --verso-code-color: #bdbdbd;
    --verso-code-keyword-color: #6c95eb;
    --verso-code-const-color: #c191ff;
    --verso-code-var-color: #bdbdbd;
    --verso-code-ctor-color: #65c3cc;
    --verso-code-def-color: #3acc9b;
    --verso-code-string-color: #c8a16d;
    --verso-code-number-color: #ec94c0;
    --verso-code-comment-color: #85c46c;
    /* The clone's doc-comment green #477D33 is only 3.1:1 here, so doc
       comments share the readable comment green instead. */
    --verso-code-doc-color: #85c46c;
    --verso-code-punct-color: #bdbdbd;
    --verso-code-annotation-color: #65c3cc;
    --verso-code-hover-bg-color: #43454a;
    --verso-inline-code-bg: #2b2d30;
    --verso-selected-color: #09335e;

    /* Tooltips, proof states, diagnostics */
    --verso-tooltip-color: #bdbdbd;
    --verso-tooltip-bg-color: #2b2d30;
    --verso-tooltip-border-color: #393b41;
    --verso-tooltip-separator-color: #393b41;
    --verso-tactic-state-color: var(--verso-tooltip-color);
    --verso-tactic-state-bg-color: var(--verso-tooltip-bg-color);
    --verso-tactic-state-border-color: var(--verso-tooltip-border-color);
    --verso-tactic-toggle-color: #9fa1a5;
    --verso-tactic-toggle-checked-color: #82acfc;
    --verso-info-indicator-color: #6c95eb;
    --verso-code-info-hover-bg-color: #2e436e;
    --verso-tooltip-info-border-color: #3474f0;
    --verso-message-info-color: var(--verso-tooltip-color);
    --verso-output-info-color: var(--verso-info-indicator-color);
    --verso-warning-indicator-color: #e8b34b;
    --verso-code-warning-hover-bg-color: #4a3d1f;
    --verso-tooltip-warning-border-color: #6b5a2e;
    --verso-message-warning-color: #e8b34b;
    --verso-output-warning-color: var(--verso-warning-indicator-color);
    --verso-error-indicator-color: #f26d6d;
    --verso-code-error-hover-bg-color: #4d2a2a;
    --verso-tooltip-error-border-color: #6e3a3a;
    --verso-message-error-color: #f26d6d;
    --verso-output-error-color: var(--verso-error-indicator-color);

    /* Remaining chrome */
    --verso-imports-summary-color: var(--verso-muted-color);
    --verso-output-color: var(--verso-code-color);
    --verso-blockquote-color: #9fa1a5;
    --verso-blockquote-border-color: #393b41;
    --verso-docstring-border-color: var(--verso-border-color);
    --verso-copy-button-bg: var(--verso-surface-color);
    --verso-copy-button-color: var(--verso-muted-color);
    --verso-copy-button-border: var(--verso-border-color);
    --verso-copy-button-hover-bg: var(--verso-code-hover-bg-color);
    --verso-copy-button-copied-color: #85c46c;
    --verso-hamburger-bg: var(--verso-surface-color);
    --verso-hamburger-border: var(--verso-border-color);
    --verso-hamburger-bar-color: var(--verso-text-color);
  }
}

/* Syntax tokens Verso does not expose as variables. Verso maps these token
   kinds to the plain code colour; give each Rider/Light-Warm role its colour. */
.hl.lean .literal.string,
.hl.lean .literal.char { color: var(--verso-code-string-color); }
.hl.lean .literal.number,
.hl.lean .number { color: var(--verso-code-number-color); }
.hl.lean .comment { color: var(--verso-code-comment-color); font-style: italic; }
.hl.lean .doc-comment { color: var(--verso-code-doc-color); font-style: italic; }
.hl.lean .sort { color: var(--verso-code-const-color); }
/* Kinds within Verso's single `const` class, tagged by const-kinds.js from
   the Lean environment: types keep the const colour above. */
.hl.lean .const-ctor { color: var(--verso-code-ctor-color); }
.hl.lean .const-def { color: var(--verso-code-def-color); }
.hl.lean .option { color: var(--verso-code-annotation-color); }
.hl.lean .punctuation,
.hl.lean .delim,
.hl.lean .wildcard { color: var(--verso-code-punct-color); }
::selection { background: var(--verso-selected-color); }

/* Preserve Verso's scrollable navigation and mobile menu; center the article. */
.main-area, .content-wrapper, .code-content { min-width: 0; }
.sidebar { width: 16rem; }
.module-tree, .breadcrumbs { font-family: var(--verso-structure-font-family); }
.module-tree { line-height: 1.65; }
.module-tree .leaf, .module-tree summary { padding-block: .4rem; }
.title-bar { padding-block: .7rem; }
.page-toc { width: 12rem; font-family: var(--verso-structure-font-family); }
.code-content { padding: 3rem clamp(1.25rem, 4vw, 5rem) 6rem; }
.code-content > * { max-width: 46rem; margin-inline: auto; }
.code-content > :is(.md-text.mod-doc, .verso-text.mod-doc) {
  max-width: 46rem;
  font-size: 1.125rem;
  line-height: 1.85;
  margin-bottom: 1.8rem;
  overflow-wrap: break-word;
}
.code-content > :is(.md-text.mod-doc, .verso-text.mod-doc) :is(p, ul, ol, blockquote) {
  margin-bottom: 1.1em;
}
.code-content > :is(.md-text.mod-doc, .verso-text.mod-doc) h1 {
  font-family: var(--verso-text-font-family);
  font-size: clamp(2rem, 3vw, 2.7rem);
  font-weight: 500;
  line-height: 1.2;
  letter-spacing: -.025em;
  border: 0;
  margin: .4rem 0 1.6rem;
  padding: 0;
  text-wrap: balance;
}
.code-content > :is(.md-text.mod-doc, .verso-text.mod-doc) :is(h2, h3) {
  font-family: var(--verso-text-font-family);
  line-height: 1.3;
  margin-top: 2.2rem;
  margin-bottom: 1rem;
}
.code-content > :is(.md-text.mod-doc, .verso-text.mod-doc) a {
  text-underline-offset: .18em;
}
.code-content > :is(.md-text.mod-doc, .verso-text.mod-doc) code { font-size: .83em; }
/* Centre prose images (the home-page knot) and keep them compact. */
.code-content :is(.md-text, .verso-text) img {
  display: block;
  margin-inline: auto;
  width: 100%;
  max-width: 340px;
  height: auto;
}
.code-box {
  padding: 1.25rem 1.4rem;
  margin-bottom: 2.25rem;
  border-radius: .2rem;
  font-size: .875rem;
  line-height: 1.7;
  color: var(--verso-code-color);
}
.hl.lean, .hl.lean a { color: var(--verso-code-color); }
.hl.lean.popup {
  color: var(--verso-tooltip-color);
  background: var(--verso-tooltip-bg-color);
}
.hl.lean .hover-info.messages > :is(code.error, code.warning, code.information) {
  background: var(--verso-tooltip-bg-color);
}
.imports-list { font-family: var(--verso-structure-font-family); }
/* Keep mathematical layout and fonts supplied by KaTeX, with room for fractions. */
.katex { color: var(--verso-text-color); font-size: 1.08em; }
.katex-display {
  margin: 1.8em 0;
  padding: .4em 0;
  overflow-x: auto;
  overflow-y: hidden;
}
@media (max-width: 1100px) { .page-toc { display: none; } }
@media (max-width: 768px) {
  .sidebar { width: 280px; left: -280px; }
  .code-content { padding: 1.6rem 1.1rem 4rem; }
  .code-content > :is(.md-text.mod-doc, .verso-text.mod-doc) { font-size: 1.0625rem; line-height: 1.75; }
  .code-box { padding: 1rem; font-size: .8125rem; }
}
@media print {
  :root { color-scheme: light; }
  body, .layout, .main-area, .content-wrapper, .code-content { height: auto; overflow: visible; display: block; }
  body, .code-content, .code-box { background: white; color: black; }
  .sidebar, .title-bar, .page-toc, .hamburger, .copy-button, .imports-list { display: none; }
  .code-content { padding: 0; }
  .code-box { white-space: pre-wrap; break-inside: avoid; }
  .hl.lean, .hl.lean * { color: black !important; }
  .code-content > :is(.md-text.mod-doc, .verso-text.mod-doc) { font-size: 11pt; }
}

/* Keep search in normal flow so it never covers the chapter breadcrumb. */
.title-bar { display: grid; grid-template-columns: minmax(0, 1fr) minmax(10rem, 18rem); gap: 1rem; align-items: center; }
.title-bar #search-wrapper { position: relative; width: 100%; padding: 0; }
.title-bar #search-wrapper .combobox-list,
.title-bar #search-wrapper .combobox .cb_edit,
.title-bar #search-wrapper ul[role="listbox"] { width: 100%; }
.hl.lean { font-family: var(--verso-code-font-family); }
@media (max-width: 1000px) {
  .title-bar { grid-template-columns: minmax(0, 1fr); gap: .5rem; }
  .title-bar #search-wrapper { max-width: 24rem; }
}
@media print { .title-bar { display: none; } }

/* Verso 4.35's Markdown renderer emits list items as <p> inside <ul>/<ol>
   without <li>, so browsers show no bullets or numbers. Treat those
   paragraphs as list items; this also fixes the numbered lists in the
   Syntax and FunZero indexes. */
.code-content > :is(.md-text.mod-doc, .verso-text.mod-doc) :is(ul, ol) > p,
.code-content .code-box :is(.md-text, .verso-text) :is(ul, ol) > p {
  display: list-item;
  margin-bottom: .3em;
}