/* Page styling of the interactive report.
   Colour rule: no red and no green anywhere.  State is carried by the blue accent or by amber,
   and always by a shape or by text as well. */

:root {
  --bg: #fbfaf7;
  --fg: #1c1d21;
  --muted: #666b78;
  --line: #d9d6cd;
  --accent: #2f5fe0;          /* RoyalBlue family */
  --warn: #b06a00;            /* amber */
  --panel: #f2f0ea;
  --code-bg: #eceae3;

  --accent-soft: rgba(47, 95, 224, 0.10);
  --warn-soft: rgba(176, 106, 0, 0.12);
  --mon: #2f5fe0;             /* the monitor's contribution in the step rules */
  --acct: #7b7f8a;            /* the per-region account in the step rules */
  --shadow: 0 6px 28px rgba(20, 24, 40, 0.18);

  --text-width: 46rem;
  --sidebar-width: 17rem;
  --topbar-height: 2.75rem;
  --gutter: 16px;

  --serif: "Iowan Old Style", "Palatino Linotype", Palatino, "Book Antiqua", Georgia, serif;
  --sans: -apple-system, BlinkMacSystemFont, "Segoe UI", "Helvetica Neue", Arial, sans-serif;
  --mono: ui-monospace, "SF Mono", SFMono-Regular, Menlo, Consolas, "DejaVu Sans Mono", monospace;
}

@media (prefers-color-scheme: dark) {
  :root:not([data-theme="light"]) {
    --bg: #15171c;
    --fg: #e4e5ea;
    --muted: #9a9fad;
    --line: #333742;
    --accent: #7ea2ff;
    --warn: #f0b34a;
    --panel: #1d2027;
    --code-bg: #24272f;
    --accent-soft: rgba(126, 162, 255, 0.14);
    --warn-soft: rgba(240, 179, 74, 0.14);
    --mon: #7ea2ff;
    --acct: #8d92a0;
    --shadow: 0 6px 28px rgba(0, 0, 0, 0.55);
  }
}

:root[data-theme="dark"] {
  --bg: #15171c;
  --fg: #e4e5ea;
  --muted: #9a9fad;
  --line: #333742;
  --accent: #7ea2ff;
  --warn: #f0b34a;
  --panel: #1d2027;
  --code-bg: #24272f;
  --accent-soft: rgba(126, 162, 255, 0.14);
  --warn-soft: rgba(240, 179, 74, 0.14);
  --mon: #7ea2ff;
  --acct: #8d92a0;
  --shadow: 0 6px 28px rgba(0, 0, 0, 0.55);
}

*, *::before, *::after { box-sizing: border-box; }

html {
  scroll-padding-top: calc(var(--topbar-height) + 1rem);
  -webkit-text-size-adjust: 100%;
  text-size-adjust: 100%;
}

body {
  margin: 0;
  background: var(--bg);
  color: var(--fg);
  font-family: var(--serif);
  font-size: 1.0625rem;
  line-height: 1.65;
  overflow-x: hidden;
}

a { color: var(--accent); text-decoration-thickness: 1px; text-underline-offset: 2px; }
a:focus-visible, button:focus-visible { outline: 2px solid var(--accent); outline-offset: 2px; }

/* ---------------------------------------------------------------- top bar */

.topbar {
  position: sticky;
  top: 0;
  z-index: 30;
  height: var(--topbar-height);
  display: flex;
  align-items: center;
  gap: 0.75rem;
  padding: 0 var(--gutter);
  background: var(--bg);
  border-bottom: 1px solid var(--line);
  font-family: var(--sans);
  font-size: 0.875rem;
}

.topbar-title {
  flex: 1 1 auto;
  min-width: 0;
  overflow: hidden;
  white-space: nowrap;
  text-overflow: ellipsis;
  color: var(--muted);
  text-decoration: none;
}

.icon-btn {
  flex: 0 0 auto;
  display: inline-flex;
  align-items: center;
  gap: 0.4rem;
  height: 2rem;
  padding: 0 0.6rem;
  border: 1px solid var(--line);
  border-radius: 6px;
  background: var(--panel);
  color: var(--fg);
  font: inherit;
  cursor: pointer;
}
.icon-btn:hover { border-color: var(--accent); }
#toc-toggle { display: none; }

/* ---------------------------------------------------------------- layout */

.layout {
  display: grid;
  grid-template-columns: var(--sidebar-width) minmax(0, 1fr);
  align-items: start;
}

.sidebar {
  position: sticky;
  top: var(--topbar-height);
  height: calc(100vh - var(--topbar-height));
  overflow-y: auto;
  overscroll-behavior: contain;
  padding: 1rem 0.5rem 2rem var(--gutter);
  border-right: 1px solid var(--line);
  font-family: var(--sans);
  font-size: 0.8125rem;
  line-height: 1.35;
}

.sidebar ol { list-style: none; margin: 0; padding: 0; }
.sidebar li { margin: 0; }
.sidebar ol ol { margin: 0 0 0.35rem 0; }
.sidebar a {
  display: flex;
  gap: 0.5rem;
  padding: 0.22rem 0.5rem;
  border-left: 3px solid transparent;
  border-radius: 0 4px 4px 0;
  color: var(--fg);
  text-decoration: none;
}
.sidebar a:hover { background: var(--panel); }
.sidebar .toc-num { flex: 0 0 auto; min-width: 1.6em; color: var(--muted); font-variant-numeric: tabular-nums; }
.sidebar .toc-sec > a { font-weight: 600; margin-top: 0.3rem; }
.sidebar .toc-sub > a { padding-left: 1.1rem; color: var(--muted); }
.sidebar a.active {
  border-left-color: var(--accent);
  background: var(--accent-soft);
  color: var(--fg);
}
.sidebar a.active .toc-num { color: var(--accent); }

.report {
  min-width: 0;
  width: 100%;
  max-width: calc(var(--text-width) + 2 * var(--gutter) + 4rem);
  margin: 0 auto;
  padding: 1.5rem calc(var(--gutter) + 2rem) 6rem;
}

/* ---------------------------------------------------------------- text */

.doc-title {
  font-size: 1.9rem;
  line-height: 1.2;
  font-weight: 600;
  text-align: center;
  margin: 1.5rem 0 2rem;
}

h2, h3, h4 { font-family: var(--sans); line-height: 1.25; }
h2.section {
  font-size: 1.45rem;
  margin: 3.5rem 0 0.75rem;
  padding-top: 1.25rem;
  border-top: 1px solid var(--line);
}
h3.subsection { font-size: 1.15rem; margin: 2.25rem 0 0.6rem; }
h4.para { font-size: 1rem; margin: 1.6rem 0 0.3rem; }
.secnum { color: var(--accent); margin-right: 0.45em; font-variant-numeric: tabular-nums; }

p { margin: 0.7rem 0; }
/* MathJax does not break an inline formula; a line that a long formula makes wider than the
   column scrolls inside its own paragraph instead of widening the page */
main p, main dt, main td, main th, main figcaption { overflow-x: auto; overflow-y: hidden; }
ul, ol { padding-left: 1.6rem; }
li > p { margin: 0.3rem 0; }

em em { font-style: normal; }
.nodecor { font-weight: normal; font-style: normal; }
.smallcaps { font-variant: small-caps; font-style: normal; letter-spacing: 0.02em; }
a.ruleref { text-decoration: none; }
a.ruleref:hover .smallcaps, a.xref:hover { text-decoration: underline; }
a.xref { text-decoration: none; font-variant-numeric: tabular-nums; }

code, pre, .tt { font-family: var(--mono); }
code {
  font-size: 0.86em;
  padding: 0.05em 0.25em;
  border-radius: 3px;
  background: var(--code-bg);
  overflow-wrap: break-word;
}
.nw { white-space: nowrap; }
em code { font-style: normal; }

pre.listing {
  margin: 0.8rem 0;
  padding: 0.7rem 0.9rem;
  border: 1px solid var(--line);
  border-radius: 6px;
  background: var(--code-bg);
  font-size: 0.82rem;
  line-height: 1.5;
  font-style: normal;
  overflow-x: auto;
  white-space: pre;
  tab-size: 4;
}
/* a symbol of a mathescape listing occupies one character cell */
pre.listing .sym { display: inline-block; width: 1ch; text-align: center; }

blockquote { margin: 0.8rem 0 0.8rem 1.5rem; padding: 0; }
blockquote.tt { font-size: 0.82rem; line-height: 1.5; overflow-x: auto; }
blockquote.tt p { white-space: nowrap; }

.small-note { font-size: 0.85rem; color: var(--muted); margin-top: 3rem; border-top: 1px solid var(--line); padding-top: 1rem; }

/* coloured running text of the step-rule legend */
.mon { color: var(--mon); }
.acct { color: var(--acct); }

/* ---------------------------------------------------------------- provenance, example footers */

.provenance { display: flex; flex-direction: column; gap: 0.2rem; margin: 0.4rem 0 1.1rem; }
.prov-chip, .leanexample {
  font-family: var(--mono);
  font-size: 0.72rem;
  line-height: 1.5;
  color: var(--muted);
  overflow-wrap: anywhere;
}
.prov-chip {
  align-self: flex-start;
  padding: 0.1rem 0.5rem;
  border: 1px solid var(--line);
  border-radius: 999px;
  cursor: default;
}
.prov-chip code, .leanexample code { background: none; padding: 0; font-size: 1em; color: inherit; }
.prov-chip .sep, .leanexample .sep { margin: 0 0.4em; }
.leanexample { margin: 0.6rem 0 0; padding-top: 0.4rem; border-top: 1px dashed var(--line); font-style: normal; }

/* ---------------------------------------------------------------- narration markers */

.llmnarr::before { content: "\00AB"; color: var(--accent); }
.llmnarr::after  { content: "\00BB"; color: var(--accent); }
p.llmnarr-par, .llmnarrative {
  border-left: 3px solid var(--accent);
  padding-left: 0.9rem;
}
.llmnarrative { margin: 1rem 0; }
.llmnarrative-tag {
  margin: 0;
  font-family: var(--sans);
  font-size: 0.75rem;
  color: var(--accent);
}

/* ---------------------------------------------------------------- theorem-like blocks */

div.definition, div.lemma, div.theorem, div.example {
  position: relative;
  margin: 1.3rem 0;
  padding: 0.7rem 1rem 0.8rem;
  border: 1px solid var(--line);
  border-left-width: 3px;
  border-radius: 4px;
  background: var(--panel);
}
div.lemma   { border-left-style: double; border-left-width: 5px; }
div.theorem { border-color: var(--accent); border-left-width: 5px; }
div.example { background: transparent; border-left-style: dashed; }

.thm-label {
  font-family: var(--sans);
  font-size: 0.82em;
  font-weight: 700;
  letter-spacing: 0.02em;
  text-transform: uppercase;
  font-style: normal;
}
div.theorem .thm-label { color: var(--accent); }
.thm-title { font-style: normal; font-weight: 600; }
.thm-dot { font-style: normal; margin-right: 0.3em; }

a.anchor {
  margin-left: 0.35em;
  font-family: var(--sans);
  font-size: 0.8em;
  font-style: normal;
  text-decoration: none;
  color: var(--muted);
  opacity: 0;
}
div:hover > p > a.anchor, a.anchor:focus-visible { opacity: 1; }
@media (hover: none) { a.anchor { opacity: 0.6; } }

.lean-name { float: right; margin-left: 1em; font-style: normal; }

:target { scroll-margin-top: calc(var(--topbar-height) + 1rem); }
div.definition:target, div.lemma:target, div.theorem:target, div.example:target,
figure:target, .rule:target, .flash {
  outline: 2px solid var(--accent);
  outline-offset: 3px;
}

/* ---------------------------------------------------------------- lists with their own labels */

dl { margin: 0.7rem 0; }
dt { font-weight: 700; margin-top: 0.6rem; }
dd { margin: 0.15rem 0 0.4rem 1.5rem; }
dd > p:first-child { margin-top: 0; }
/* an itemize whose items carry their own tags: tag column and text column, as in the PDF */
dl.tagged {
  display: grid;
  grid-template-columns: max-content minmax(0, 1fr);
  column-gap: 0.9rem;
  row-gap: 0.3rem;
  align-items: baseline;
}
dl.tagged > dt { font-weight: 400; font-style: normal; margin: 0; }
dl.tagged > dd { margin: 0; min-width: 0; }
dl.tagged > dd > p { margin: 0; }

/* ---------------------------------------------------------------- formulas */

/* a wide display scrolls inside its own box */
span.math.display {
  display: block;
  max-width: 100%;
  overflow-x: auto;
  overflow-y: hidden;
  padding: 0.25rem 0;
}
span.math.display > mjx-container[display="true"] { margin: 0.5em 0 !important; min-width: max-content; }
mjx-container { font-style: normal; }
/* MathJax paints an error node in its own colours; here it is amber with a dotted frame */
mjx-merror, mjx-container [data-mjx-error] {
  color: var(--warn) !important;
  background: var(--warn-soft) !important;
  border: 1px dotted var(--warn) !important;
}

/* ---------------------------------------------------------------- inference rules */

.mathpar {
  display: flex;
  flex-wrap: wrap;
  justify-content: center;
  align-items: flex-end;
  gap: 1.6rem 2.2rem;
  margin: 1rem 0;
  font-style: normal;
  font-size: 0.9rem;
  line-height: 1.5;
}
.rule-row-break { flex: 0 0 100%; height: 0; margin-top: -1.6rem; }

/* the rule name sits above the rule at its left end, as mathpartir sets it */
.rule {
  display: flex;
  flex-direction: column;
  align-items: flex-start;
  gap: 0.05rem;
  max-width: 100%;
  min-width: 0;
  border-radius: 3px;
}
.rule-name {
  flex: 0 0 auto;
  font-family: var(--serif);
  font-variant: small-caps;
  letter-spacing: 0.02em;
  color: var(--muted);
  white-space: nowrap;
}
.rule-body { min-width: 0; max-width: 100%; overflow-x: auto; overflow-y: hidden; }
.premises {
  display: flex;
  flex-wrap: wrap;
  justify-content: center;
  align-items: baseline;
  gap: 0.35rem 1.5rem;
  min-height: 0.6rem;
  padding: 0 0.6rem 0.3rem;
}
.prem { white-space: nowrap; }
.prem-break { flex: 0 0 100%; height: 0; }
.conclusion {
  border-top: 1.5px solid var(--fg);
  padding: 0.3rem 0.6rem 0;
  text-align: center;
  min-width: max-content;
}
.concl-line { white-space: nowrap; }
.concl-line + .concl-line { text-align: left; }

/* ---------------------------------------------------------------- figures, tables */

figure {
  margin: 2rem 0;
  padding: 1rem 0.9rem;
  border: 1px solid var(--line);
  border-radius: 6px;
}
figure > p { font-size: 0.92rem; }
figcaption {
  margin-top: 0.9rem;
  padding-top: 0.6rem;
  border-top: 1px solid var(--line);
  font-size: 0.9rem;
  color: var(--muted);
}
.fig-label { font-family: var(--sans); font-weight: 700; font-size: 0.85em; color: var(--fg); }

.center { display: block; }
.table-wrap { max-width: 100%; overflow-x: auto; margin: 1rem 0; }
table {
  border-collapse: collapse;
  margin: 0 auto;
  font-size: 0.88rem;
  line-height: 1.45;
  font-style: normal;
}
th, td { padding: 0.35rem 0.7rem; vertical-align: top; border-bottom: 1px solid var(--line); }
th { font-family: var(--sans); font-weight: 600; text-align: left; border-bottom: 1.5px solid var(--fg); }
th em, td em { font-style: normal; }
table:has(colgroup) { width: 100%; table-layout: fixed; }

/* ---------------------------------------------------------------- cross-reference preview */

.xref-pop {
  position: absolute;
  z-index: 50;
  width: min(42rem, calc(100vw - 2 * var(--gutter)));
  max-height: min(60vh, 34rem);
  overflow: auto;
  padding: 0.6rem 0.9rem 0.7rem;
  border: 1px solid var(--line);
  border-top: 3px solid var(--accent);
  border-radius: 6px;
  background: var(--bg);
  box-shadow: var(--shadow);
  font-size: 0.92rem;
  line-height: 1.55;
}
.xref-pop[hidden] { display: none; }
.xref-pop-head {
  display: flex;
  justify-content: space-between;
  align-items: baseline;
  gap: 1rem;
  margin-bottom: 0.3rem;
  font-family: var(--sans);
  font-size: 0.75rem;
  color: var(--muted);
}
.xref-pop-head a { white-space: nowrap; }
.xref-pop-body > :first-child { margin-top: 0.2rem; }
.xref-pop-body > :last-child { margin-bottom: 0; }
.xref-pop div.definition, .xref-pop div.lemma, .xref-pop div.theorem, .xref-pop div.example,
.xref-pop figure { margin: 0; border: 0; padding: 0; background: none; }
.xref-pop h2, .xref-pop h3 { margin: 0.2rem 0 0.4rem; padding: 0; border: 0; font-size: 1.05rem; }
.xref-pop a.anchor { display: none; }
.xref-pop .mathpar { justify-content: flex-start; }

/* the way back after a jump */
.back-btn {
  position: fixed;
  left: calc(var(--sidebar-width) + 1rem);
  bottom: 1.1rem;
  z-index: 40;
  display: inline-flex;
  align-items: center;
  gap: 0.45rem;
  max-width: calc(100vw - 2 * var(--gutter));
  padding: 0.45rem 0.8rem;
  border: 1px solid var(--accent);
  border-radius: 999px;
  background: var(--bg);
  color: var(--accent);
  box-shadow: var(--shadow);
  font-family: var(--sans);
  font-size: 0.8125rem;
  cursor: pointer;
}
.back-btn[hidden] { display: none; }
.back-btn .back-what { overflow: hidden; white-space: nowrap; text-overflow: ellipsis; color: var(--fg); }

.mathjax-note {
  position: fixed;
  right: var(--gutter);
  bottom: 1.1rem;
  z-index: 40;
  max-width: 22rem;
  padding: 0.5rem 0.8rem;
  border: 1px dashed var(--warn);
  border-radius: 6px;
  background: var(--bg);
  color: var(--warn);
  font-family: var(--sans);
  font-size: 0.8125rem;
}

/* ---------------------------------------------------------------- narrow screens */

@media (max-width: 960px) {
  #toc-toggle { display: inline-flex; }
  .layout { display: block; }
  .sidebar {
    position: fixed;
    top: var(--topbar-height);
    left: 0;
    z-index: 25;
    width: min(20rem, 86vw);
    background: var(--bg);
    box-shadow: var(--shadow);
    transform: translateX(-105%);
    visibility: hidden;
    transition: transform 0.18s ease, visibility 0.18s;
  }
  body.toc-open .sidebar { transform: none; visibility: visible; }
  .report { padding: 1rem var(--gutter) 5rem; }
  .back-btn { left: var(--gutter); }
}

@media (max-width: 560px) {
  body { font-size: 1rem; }
  .btn-text { display: none; }
  .doc-title { font-size: 1.5rem; }
  div.definition, div.lemma, div.theorem, div.example { padding: 0.6rem 0.7rem 0.7rem; }
  figure { padding: 0.7rem 0.5rem; }
  .lean-name { float: none; display: block; margin: 0.15rem 0 0; }
  dd { margin-left: 0.9rem; }
  dl.tagged { display: block; }
  dl.tagged > dt { margin-top: 0.5rem; }
  dl.tagged > dd { margin-left: 0.9rem; }
}

@media (prefers-reduced-motion: reduce) {
  .sidebar { transition: none; }
  html { scroll-behavior: auto; }
}