/* MiniLean4 ebook stylesheet.
   Near-black paper, one yellow accent, monospace display type, terminals as
   the central object. Red and green appear only for failure and success. */

@font-face { font-family: "IBM Plex Sans"; font-weight: 400; font-display: swap; src: url("fonts/sans-400.woff2") format("woff2"); }
@font-face { font-family: "IBM Plex Sans"; font-weight: 500; font-display: swap; src: url("fonts/sans-500.woff2") format("woff2"); }
@font-face { font-family: "IBM Plex Sans"; font-weight: 600; font-display: swap; src: url("fonts/sans-600.woff2") format("woff2"); }
@font-face { font-family: "IBM Plex Mono"; font-weight: 400; font-display: swap; src: url("fonts/mono-400.woff2") format("woff2"); }
@font-face { font-family: "IBM Plex Mono"; font-weight: 500; font-display: swap; src: url("fonts/mono-500.woff2") format("woff2"); }

:root {
  --bg: #0b0d10;
  --bg2: #111419;
  --bg3: #15191f;
  --well: #07090b;
  --fg: #e8e6e1;
  --fg2: #c9cdd3;
  --muted: #8a9099;
  --dim: #5c636d;
  --border: #23272e;
  --border2: #3a3f47;
  --accent: #62d38f;
  --accent-solid: #1f9d55;
  --accent-ink: #ffffff;
  --accent-soft: rgba(31, 157, 85, .45);
  --accent-glow: rgba(98, 211, 143, .7);
  --bad: #ff6258;
  --warn: #d6a94e;
  --ok: #8be3b1;
  --info: #a9bdd0;
  --shadow: 0 40px 100px rgba(0, 0, 0, .65);
  --shadow-sm: 0 18px 40px rgba(0, 0, 0, .45);

  --mono: "IBM Plex Mono", "SF Mono", ui-monospace, Menlo, Consolas, monospace;
  --sans: "IBM Plex Sans", -apple-system, system-ui, "Inter", Helvetica, Arial, sans-serif;

  --sidebar-w: 17rem;
  --margin-w: 13rem;
  --content-w: 48rem;
  --r: 12px;
}

html.light {
  --bg: #f4f3ee;
  --bg2: #ffffff;
  --bg3: #e9e8e1;
  --well: #fbfaf7;
  --fg: #16181c;
  --fg2: #33363c;
  --muted: #6a717c;
  --dim: #9097a1;
  --border: #dddcd4;
  --border2: #c3c2ba;
  --accent: #1d7f46;
  --accent-solid: #1d7f46;
  --accent-ink: #ffffff;
  --accent-soft: rgba(29, 127, 70, .35);
  --accent-glow: rgba(29, 127, 70, .4);
  --bad: #c0261d;
  --warn: #9a7210;
  --ok: #1d7f46;
  --info: #2f5f8c;
  --shadow: 0 30px 70px rgba(30, 30, 20, .18);
  --shadow-sm: 0 12px 30px rgba(30, 30, 20, .14);
}

* { box-sizing: border-box; }

html {
  background: var(--bg);
  color: var(--fg);
  font: 17px/1.6 var(--sans);
  -webkit-font-smoothing: antialiased;
  -webkit-text-size-adjust: 100%;
}

body { margin: 0; overflow-x: hidden; }

::selection { background: var(--accent-solid); color: #fff; }

a { color: var(--accent); text-decoration: none; border-bottom: 1px solid var(--accent-soft); }
a:hover { border-bottom-color: var(--accent); }
a:focus-visible, button:focus-visible, textarea:focus-visible, summary:focus-visible, [tabindex]:focus-visible {
  outline: 2px solid var(--accent);
  outline-offset: 2px;
}

.skip { position: absolute; left: -999px; top: 0; background: var(--bg2); padding: .5rem 1rem; z-index: 10; }
.skip:focus { left: 1rem; }

/* ---------- Shell: rail + main ---------- */

.shell { display: flex; min-height: 100vh; }

.sidebar {
  width: var(--sidebar-w);
  flex: 0 0 auto;
  position: sticky;
  top: 0;
  height: 100vh;
  overflow-y: auto;
  border-right: 1px solid var(--border);
  padding: 1.6rem 1.1rem 2rem 1.3rem;
  font-size: .84rem;
  scrollbar-width: thin;
}

.sidebar-head { margin-bottom: 1.6rem; }
.logo {
  display: inline-block;
  font: 700 1.55rem/1 var(--mono);
  letter-spacing: -.05em;
  color: var(--fg);
  border: 0;
}
.logo:hover { border: 0; }
/* The square beside the logo keeps the h5i.dev red on purpose; everything else is green. */
.logo::after { content: ""; display: inline-block; width: .32em; height: .32em; margin-left: .18em; background: #e0241b; vertical-align: .08em; }
.book-sub { margin: .55rem 0 0; color: var(--muted); font-size: .8rem; line-height: 1.35; max-width: 15rem; }

.toc-cover, .toc-print {
  display: block; color: var(--muted); padding: .25rem 0; border: 0; font-family: var(--mono); font-size: .76rem;
}
.toc-cover:hover, .toc-print:hover { color: var(--accent); border: 0; }
.toc-part {
  margin: 1.3rem 0 .35rem;
  font: 600 .7rem var(--mono);
  letter-spacing: .12em;
  text-transform: uppercase;
  color: var(--dim);
}

/* The rail: a track with one dot per chapter. Past chapters are filled and
   dimmed, the current one is lit, the rest are hollow. */
.toc-list { list-style: none; margin: 0; padding: 0; position: relative; }
.toc-list::before { content: ""; position: absolute; left: 5px; top: .4rem; bottom: .4rem; width: 1px; background: var(--border); }
.toc-list li { position: relative; margin: 0; }
.toc-list li a {
  display: flex; gap: .55rem; align-items: flex-start;
  padding: .3rem .4rem .3rem 1.25rem;
  color: var(--fg2);
  border: 0;
  border-radius: 6px;
  line-height: 1.3;
}
.toc-list li a::before {
  content: ""; position: absolute; left: 1px; top: .72rem; width: 9px; height: 9px;
  border-radius: 50%; border: 1.5px solid var(--border2); background: var(--bg);
  transition: border-color .3s, background .3s, box-shadow .3s;
}
.toc-list li a:hover { color: var(--fg); background: var(--bg2); }
.toc-list li.past a { color: var(--muted); }
.toc-list li.past a::before { border-color: var(--accent); background: var(--accent); opacity: .5; }
.toc-list li.current a { color: var(--fg); font-weight: 500; }
.toc-list li.current a::before {
  border-color: var(--accent); background: var(--accent);
  box-shadow: 0 0 0 4px rgba(31, 157, 85, .18), 0 0 16px var(--accent-glow);
}
.toc-num { flex: 0 0 1.2rem; text-align: right; color: var(--dim); font: 500 .74rem/1.55 var(--mono); }
.toc-list li.current .toc-num { color: var(--accent); }

.main { flex: 1 1 auto; min-width: 0; display: flex; flex-direction: column; }

.topbar {
  display: flex; align-items: center; gap: .6rem;
  padding: .6rem 1.3rem;
  position: sticky; top: 0; z-index: 5;
  background: linear-gradient(var(--bg) 70%, transparent);
}
.topbar-spacer { flex: 1; }
.topbar-btn, .stepper-btn, .playground-reset {
  font: 600 .78rem var(--mono);
  color: var(--fg);
  background: var(--bg2);
  border: 1px solid var(--border);
  border-radius: 999px;
  padding: .35rem .85rem;
  cursor: pointer;
  transition: border-color .2s, transform .1s;
}
.topbar-btn:hover, .stepper-btn:hover:not(:disabled), .playground-reset:hover { border-color: var(--accent); }
.topbar-btn:active, .stepper-btn:active, .playground-reset:active { transform: scale(.96); }
#nav-toggle { display: none; }
.topbar-link { display: inline-flex; align-items: center; gap: .4rem; margin-right: .4rem; border-bottom: 1px solid var(--border); }
.topbar-icon { padding: .3rem .55rem; }
.topbar-icon svg { width: 15px; height: 15px; display: block; }
.topbar-link:hover { color: var(--accent); border-color: var(--accent); }

.layout {
  display: flex;
  gap: 2.8rem;
  padding: 1.2rem 2.6rem 4rem;
  max-width: calc(var(--content-w) + var(--margin-w) + 8rem);
  width: 100%;
  margin: 0 auto;
}

.content { flex: 1 1 auto; min-width: 0; max-width: var(--content-w); }

.margin { flex: 0 0 var(--margin-w); }
.onpage { position: sticky; top: 4rem; font-size: .78rem; }
.onpage h4 { margin: .5rem 0 .5rem; font: 600 .68rem var(--mono); letter-spacing: .12em; text-transform: uppercase; color: var(--dim); }
.onpage ol { list-style: none; margin: 0; padding: 0; border-left: 1px solid var(--border); }
.onpage li { margin: 0; }
.onpage li a { display: block; padding: .2rem .7rem; color: var(--muted); border: 0; line-height: 1.35; }
.onpage li a:hover { color: var(--accent); }

.footer {
  margin-top: auto;
  padding: 2.5rem 2.6rem 3rem;
  border-top: 1px solid var(--border);
  font: .82rem/1.7 var(--mono);
  color: var(--muted);
}
.footer p { max-width: calc(var(--content-w) + var(--margin-w) + 2.8rem); margin: 0 auto; }

/* ---------- Typography ---------- */

.chapter-head { margin: 1.2rem 0 2.4rem; }
.chapter-label {
  margin: 0 0 .5rem;
  font: 500 .82rem var(--mono);
  letter-spacing: .12em;
  text-transform: lowercase;
  color: var(--accent);
}
h1 {
  font-weight: 600;
  font-size: 2.5rem;
  line-height: 1.1;
  letter-spacing: -.025em;
  margin: 0;
}
h2 {
  font-weight: 600;
  font-size: 1.65rem;
  line-height: 1.2;
  letter-spacing: -.02em;
  margin: 3.2rem 0 1rem;
}
h3 { font-weight: 600; font-size: 1.12rem; line-height: 1.3; margin: 2.1rem 0 .6rem; }
h4 { font-weight: 600; font-size: .95rem; margin: 1.5rem 0 .4rem; }
h2 code, h3 code { font-size: .85em; color: var(--accent); }

p { margin: 0 0 1.05rem; }
.lead { font-size: 1.12rem; color: var(--fg2); margin-bottom: 1.8rem; }
.lead p { margin-bottom: .7em; }

ul, ol { padding-left: 1.4rem; margin: 0 0 1.05rem; }
li { margin-bottom: .35em; }
li > ul, li > ol { margin-top: .35em; }

strong { font-weight: 600; color: var(--fg); }
hr { border: 0; border-top: 1px solid var(--border); margin: 2.4rem 0; }

code, kbd {
  font-family: var(--mono);
  font-size: .88em;
  background: var(--bg2);
  border: 1px solid var(--border);
  border-radius: 4px;
  padding: 0 .3em;
}
pre {
  margin: 0;
  font: .84rem/1.55 var(--mono);
  overflow-x: auto;
}
pre code { background: none; border: 0; padding: 0; font-size: inherit; }

/* Code panels look like the terminals they are. */
.codeblock {
  position: relative;
  background: var(--well);
  border: 1px solid var(--border);
  border-radius: var(--r);
  padding: .9rem 1.1rem;
  margin: 0 0 1.3rem;
  box-shadow: 0 18px 50px rgba(0, 0, 0, .35);
}
html.light .codeblock { box-shadow: var(--shadow-sm); }
.codeblock::after {
  content: attr(data-lang);
  position: absolute; top: .55rem; right: .8rem;
  font: 400 .66rem var(--mono);
  letter-spacing: .08em;
  color: var(--dim);
}
.codeblock[data-lang="text"]::after { content: ""; }
.codeblock .k { color: var(--accent); font-weight: 500; }
.codeblock .c { color: var(--dim); }
.codeblock .n { color: var(--info); }
.codeblock .s { color: var(--ok); }
.codeblock .t { color: var(--info); }
.codeblock .m { color: var(--accent); }
.codeblock .a { color: var(--muted); }

table {
  border-collapse: collapse;
  margin: 0 auto 1.5rem;
  font-size: .92rem;
  font-variant-numeric: tabular-nums;
}
thead th {
  font: 600 .7rem var(--mono);
  letter-spacing: .08em;
  text-transform: uppercase;
  color: var(--muted);
  text-align: left;
  border-bottom: 1px solid var(--border2);
  padding: .4rem .8rem;
}
tbody td { padding: .4rem .8rem; border-bottom: 1px solid var(--border); vertical-align: top; }
tbody tr:last-child td { border-bottom: 1px solid var(--border2); }

.math-display {
  margin: .4em 0 1.2em;
  overflow-x: auto;
  overflow-y: hidden;
  padding: .2em 0;
}
.katex { font-size: 1.04em; }
.math-error { color: var(--bad); }

blockquote {
  margin: .4rem 0 1.1rem;
  padding: .8rem 1rem;
  border-left: 3px solid var(--accent);
  background: var(--bg2);
  font: .9rem/1.6 var(--mono);
  color: var(--fg2);
  border-radius: 0 8px 8px 0;
}

sup { line-height: 0; }
.footnote { font-size: .9rem; color: var(--fg2); border-top: 1px solid var(--border); margin-top: 2rem; }

/* ---------- Receipts: callouts with a thin left rule and a mono label ---------- */

aside.note, aside.intuition, aside.warning, aside.lean, aside.code, aside.history {
  margin: 1.6rem 0 1.8rem;
  padding: .2rem 0 .2rem 1.05rem;
  border-left: 2px solid var(--border);
  max-width: 40rem;
  font-size: .95rem;
  color: var(--fg2);
  transition: border-left-color .3s;
}
aside:hover { border-left-color: var(--accent); }
aside.note::before, aside.intuition::before, aside.warning::before, aside.lean::before, aside.code::before, aside.history::before {
  display: block;
  font: 500 .72rem var(--mono);
  letter-spacing: .08em;
  color: var(--accent);
  margin-bottom: .4rem;
}
aside.note::before { content: "note"; }
aside.intuition::before { content: "intuition"; }
aside.history::before { content: "background"; }
aside.lean::before { content: "in lean 4"; }
aside.code::before { content: "in the code"; }
aside.code { border-left-color: var(--accent-soft); }
aside.warning { border-left-color: var(--warn); }
aside.warning::before { content: "pitfall"; color: var(--warn); }
aside.warning:hover { border-left-color: var(--warn); }
aside p:last-child, aside ul:last-child, aside ol:last-child { margin-bottom: .3em; }

/* ---------- Boxes: theorems, definitions, exercises ---------- */

.theorem, .definition, .lemma, .corollary, .exercise, .rulebox, .stepper, .pager a, .contents-list li {
  background: var(--bg2);
  border: 1px solid var(--border);
  border-radius: var(--r);
}
.theorem, .definition, .lemma, .corollary {
  margin: 1.4rem 0 1.6rem;
  padding: .9rem 1.15rem;
}
.theorem p:last-child, .definition p:last-child, .lemma p:last-child, .corollary p:last-child { margin-bottom: 0; }
.theorem .math-display:last-child, .definition .math-display:last-child { margin-bottom: 0; }
.theorem { border-top: 3px solid var(--accent); }

.proof {
  margin: -.7em 0 1.8rem 0;
  padding: .2rem 0 .2rem 1.05rem;
  border-left: 1px dotted var(--border2);
  font-size: .95rem;
  color: var(--fg2);
}
.proof > p:first-child::before { content: "proof. "; font: 500 .74rem var(--mono); color: var(--muted); letter-spacing: .06em; }
.proof > :last-child::after { content: "\25A1"; float: right; margin-left: .5rem; color: var(--dim); }
.proof p:last-child { margin-bottom: 0; }

.exercise { margin: 1.4rem 0 1.6rem; padding: .9rem 1.15rem .4rem; transition: transform .2s, border-color .2s; }
.exercise:hover { border-color: var(--border2); }
.exercise > p:first-child::before { content: "exercise "; font: 500 .74rem var(--mono); letter-spacing: .08em; color: var(--accent); }
details { margin: .4em 0 .8em; }
summary {
  cursor: pointer;
  font: 500 .78rem var(--mono);
  letter-spacing: .04em;
  color: var(--accent);
  list-style: none;
  display: inline-block;
  padding: .15rem 0;
}
summary::-webkit-details-marker { display: none; }
summary::before { content: "\25B8\00a0"; }
details[open] > summary::before { content: "\25BE\00a0"; }
details > :not(summary) { margin-left: 1rem; }
details[open] > summary { margin-bottom: .4em; }

.rulebox { margin: .8rem 0 1.6rem; padding: 1rem 1.1rem .5rem; background: var(--well); }
.rulebox .math-display { margin: .2em 0 .9em; }
.rulebox .caption, .figcaption {
  font: 400 .74rem var(--mono);
  letter-spacing: .04em;
  color: var(--muted);
  margin: .2em 0 .7em;
}

.summary-box {
  margin: 3rem 0 1rem;
  padding: 1.1rem 0 .3rem;
  border-top: 1px solid var(--border);
}
.summary-box > p:first-child {
  font: 700 .82rem var(--mono);
  letter-spacing: .12em;
  text-transform: lowercase;
  color: var(--accent);
  margin-bottom: .7em;
}
.summary-box li { color: var(--fg2); }

/* ---------- Interactive widgets ---------- */

.stepper { margin: 1.6rem 0 1.8rem; overflow: hidden; box-shadow: var(--shadow-sm); }
.stepper-bar {
  display: flex; align-items: center; gap: .5rem;
  padding: .55rem .8rem;
  border-bottom: 1px solid var(--border);
  background: var(--bg3);
  font-size: .8rem;
}
.stepper-title { font: 500 .78rem var(--mono); margin-right: auto; color: var(--fg2); }
.stepper-count { font: .74rem var(--mono); color: var(--muted); min-width: 5.5rem; text-align: center; }
.stepper-btn { padding: .25rem .7rem; }
.stepper-btn:disabled { opacity: .4; cursor: default; }
.stepper-btn.active { border-color: var(--accent); color: var(--accent); }
.stepper .step { padding: 1rem 1.1rem .4rem; }
.stepper .step[hidden] { display: none; }
.stepper.show-all .step { display: block; border-bottom: 1px solid var(--border); }
.stepper.show-all .step:last-child { border-bottom: 0; }
.stepper .step-label { font: 500 .76rem var(--mono); letter-spacing: .06em; color: var(--accent); margin: 0 0 .5rem; }
.stepper.show-all .step-label::before { content: counter(step) " / "; color: var(--dim); }
.stepper.show-all { counter-reset: step; }
.stepper.show-all .step { counter-increment: step; }
.stepper .step p:last-child { margin-bottom: .5em; }

/* Goal views: an auth.log style panel. */
.goals { font: .82rem/1.55 var(--mono); margin: .4em 0 .9em; }
.goal { padding: .55rem .85rem; margin-bottom: .5rem; background: var(--well); border-radius: 8px; border: 1px solid var(--border); }
.goal-id { color: var(--dim); }
.goal-hyp { color: var(--fg2); }
.goal-target { color: var(--fg); }
.goal-target::before { content: "\22A2\00a0"; color: var(--accent); font-weight: 700; }
.goal-none { color: var(--muted); font-style: italic; }
.assign { font: .82rem var(--mono); color: var(--accent); }

/* Trace trees */
ul.trace, ul.trace ul { list-style: none; margin: 0; padding-left: 1.3rem; position: relative; }
ul.trace { padding-left: 0; margin: .6em 0 1.3em; font-size: .93rem; }
ul.trace ul { border-left: 1px solid var(--border2); margin-left: .45rem; }
ul.trace li { position: relative; margin: .28em 0; padding-left: .2rem; }
ul.trace ul > li::before { content: ""; position: absolute; left: -1.3rem; top: .85em; width: 1rem; border-top: 1px solid var(--border2); }
ul.trace li.result { color: var(--fg2); }
ul.trace li.result::after { content: ""; }
ul.trace li.fail { color: var(--bad); }
ul.trace .rule { font: 500 .68rem var(--mono); letter-spacing: .06em; color: var(--muted); margin-left: .45rem; white-space: nowrap; }
ul.trace .trace-toggle {
  font: 500 .68rem var(--mono); color: var(--accent);
  background: none; border: 0; cursor: pointer; padding: 0 .3rem; margin-left: .2rem;
}
ul.trace li.collapsed > ul { display: none; }

/* Playground: a terminal window. The bar with the three lights is drawn by
   CSS, the editor and transcript are produced by playground.js. */
.playground {
  position: relative;
  margin: 1.6rem 0 1.9rem;
  background: var(--well);
  border: 1px solid var(--border);
  border-radius: var(--r);
  overflow: hidden;
  box-shadow: var(--shadow), 0 0 0 1px rgba(31, 157, 85, .06);
  padding-top: 32px;
}
.playground::before {
  content: "";
  position: absolute; left: 0; right: 0; top: 0; height: 32px;
  background: var(--bg3);
  border-bottom: 1px solid var(--border);
}
.playground::after {
  content: "";
  position: absolute; left: 12px; top: 10px; width: 11px; height: 11px; border-radius: 50%;
  background: #ff5f57;
  box-shadow: 18px 0 0 #febc2e, 36px 0 0 #28c840;
}
.playground > pre { margin: 0; padding: .9rem 1.1rem; }
/* The editor is a transparent textarea over a highlighted copy of its text.
   Both layers share font, padding, and wrapping so the glyphs line up. */
.playground-editor-wrap { position: relative; border-bottom: 1px solid var(--border); }
.playground-editor, .playground-highlight {
  display: block;
  width: 100%;
  margin: 0;
  border: 0;
  font: 400 .84rem/1.55 var(--mono);
  padding: .9rem 1.1rem;
  tab-size: 2;
  white-space: pre-wrap;
  word-break: break-word;
  overflow-wrap: break-word;
  box-sizing: border-box;
}
.playground-highlight {
  position: absolute; inset: 0;
  overflow: hidden;
  color: var(--fg);
  pointer-events: none;
}
.playground-highlight .k { color: var(--accent); font-weight: 500; }
.playground-highlight .c { color: var(--dim); }
.playground-highlight .n { color: var(--info); }
.playground-highlight .o { color: var(--muted); }
.playground-editor {
  position: relative;
  min-height: 5rem;
  resize: vertical;
  background: transparent;
  color: transparent;
  caret-color: var(--accent);
  overflow: auto;
}
.playground-editor::selection { background: rgba(31, 157, 85, .35); color: transparent; }
.playground-editor:focus { outline: none; }
.playground-editor-wrap:focus-within { box-shadow: inset 0 0 0 1px var(--accent-soft); }
html.light .playground-editor::selection { background: rgba(29, 127, 70, .25); }
.playground-bar {
  display: flex; align-items: center; gap: .5rem;
  padding: .5rem .8rem;
  border-bottom: 1px solid var(--border);
  background: var(--bg2);
  font: .76rem var(--mono);
  color: var(--muted);
}
.playground-run {
  font: 700 .78rem var(--mono);
  color: var(--accent-ink);
  background: var(--accent-solid);
  border: 1px solid var(--accent-solid);
  border-radius: 999px;
  padding: .35rem .95rem;
  cursor: pointer;
  transition: transform .1s, filter .2s;
}
.playground-run:hover { filter: brightness(1.08); }
.playground-run:active { transform: scale(.96); }
.playground-run:disabled { opacity: .6; cursor: wait; }
.playground-hint { margin-left: auto; }
.playground-output {
  margin: 0;
  padding: .9rem 1.1rem;
  min-height: 2.6rem;
  max-height: 30rem;
  overflow: auto;
  font-size: .8rem;
  line-height: 1.6;
  color: #d7dbe0;
  white-space: pre-wrap;
  word-break: break-word;
}
html.light .playground-output { color: var(--fg); }
.playground-output:empty::before { content: "run the script to see what the kernel says."; color: var(--dim); }
.playground-output .p { color: var(--info); }
.playground-output .err { color: var(--bad); }
.playground-output .ok { color: var(--ok); }
.playground-output .dim { color: var(--muted); }
.playground-output .pw { color: var(--fg); font-weight: 500; }
.playground-output.playground-error { color: var(--fg2); }

/* ---------- Pager ---------- */

.pager {
  display: flex; gap: 1rem; justify-content: space-between;
  margin-top: 4rem; padding-top: 1.4rem;
  border-top: 1px solid var(--border);
}
.pager a {
  display: flex; flex-direction: column; gap: .15rem;
  padding: .8rem 1.1rem;
  max-width: 48%;
  color: var(--fg);
  transition: transform .2s, border-color .2s;
}
.pager a:hover { transform: translateY(-4px) rotate(-.4deg); border-color: var(--accent-soft); }
.pager-next { margin-left: auto; text-align: right; }
.pager-dir { font: .68rem var(--mono); letter-spacing: .1em; text-transform: uppercase; color: var(--muted); }
.pager-title { font-weight: 600; font-size: .95rem; }

/* ---------- Cover ---------- */

.page-cover .content { max-width: 68rem; }
.page-cover .layout { max-width: calc(68rem + 5.2rem); }
.hero {
  display: grid;
  grid-template-columns: 1.05fr 1fr;
  gap: 3rem;
  align-items: center;
  margin: 3.5rem 0 4rem;
}
.hero-head { grid-column: 1 / -1; }
.hero-text { min-width: 0; }
.hero .logo {
  font-size: clamp(3rem, 7vw, 5.8rem);
  margin: 0 0 .4rem;
  white-space: nowrap;
}
.hero .logo::after { width: .22em; height: .22em; margin-left: .14em; }
.hero-title { font-size: 1.6rem; font-weight: 600; line-height: 1.25; letter-spacing: -.02em; margin: 0 0 .6rem; max-width: 24ch; }
.byline { margin: 0 0 1.4rem; font: .82rem var(--mono); color: var(--muted); letter-spacing: .04em; }
.hero .lead { font-size: 1.05rem; margin-bottom: 1rem; }
.punch { font: 700 1.05rem var(--mono); color: var(--accent); margin: 1.4rem 0 0; }
.hero .playground {
  margin: 0;
  transform: rotate(1.2deg);
  transition: transform .4s;
}
.hero .playground:hover { transform: rotate(0) scale(1.01); }
.hero-caption { font: .82rem/1.6 var(--mono); color: var(--muted); margin: 1rem 0 0; }
.hero-caption::before { content: "\21B3 "; color: var(--dim); }

.contents { margin: 1rem 0 2rem; }
.contents-part {
  font: 600 .7rem var(--mono);
  letter-spacing: .14em;
  text-transform: uppercase;
  color: var(--dim);
  margin: 2rem 0 .8rem;
}
.contents-list { list-style: none; margin: 0; padding: 0; display: grid; grid-template-columns: repeat(3, 1fr); gap: .8rem; }
.contents-list li {
  position: relative;
  display: grid; grid-template-columns: 2rem 1fr; column-gap: .3rem;
  padding: .85rem 1rem .9rem .9rem;
  margin: 0;
  transition: transform .2s, border-color .2s;
}
.contents-list li:hover { transform: translateY(-4px) rotate(-.4deg); border-color: var(--accent-soft); }
.contents-list li a { display: contents; border: 0; }
.contents-num { font: 700 .95rem var(--mono); color: var(--accent); padding-top: .05rem; }
.contents-title { font-weight: 600; color: var(--fg); line-height: 1.3; }
.contents-desc { grid-column: 2; font-size: .86rem; color: var(--muted); margin-top: .3rem; line-height: 1.45; }

/* ---------- Print page ---------- */

.page-print .content { max-width: var(--content-w); }
.print-cover { margin: 2rem 0 4rem; }
.print-cover h1 { font-size: 2.4rem; }
.print-chapter { margin-top: 5rem; padding-top: 2.5rem; border-top: 1px solid var(--border); }
.print-chapter:first-of-type { border-top: 0; }

/* ---------- Scroll reveal (added by book.js, so no-JS pages show everything) ---------- */

.reveal { opacity: 0; transform: translateY(14px); transition: opacity .7s ease, transform .7s ease; }
.reveal.in { opacity: 1; transform: none; }

/* ---------- Responsive ---------- */

@media (max-width: 1240px) { .margin { display: none; } }

@media (max-width: 960px) {
  .hero { grid-template-columns: 1fr; min-height: 0; gap: 2rem; }
  .hero .playground { transform: none; }
  .hero .logo { white-space: normal; }
  .contents-list { grid-template-columns: 1fr 1fr; }
}
@media (max-width: 700px) { .contents-list { grid-template-columns: 1fr; } }

@media (max-width: 900px) {
  html { font-size: 16px; }
  .sidebar {
    position: fixed; left: 0; top: 0; bottom: 0; z-index: 20;
    background: var(--bg);
    transform: translateX(-100%);
    transition: transform .2s ease;
    box-shadow: 0 0 40px rgba(0, 0, 0, .6);
  }
  body.nav-open .sidebar { transform: none; }
  #nav-toggle { display: inline-block; }
  .layout { padding: 1rem 1.1rem 2.5rem; gap: 0; }
  .footer { padding: 1.6rem 1.1rem 2rem; }
  h1 { font-size: 1.9rem; }
  .pager a { max-width: 100%; }
}

@media (prefers-reduced-motion: reduce) {
  *, *::before, *::after { animation-duration: 0s !important; animation-delay: 0s !important; transition: none !important; }
  .reveal { opacity: 1; transform: none; }
}

@media print {
  .sidebar, .topbar, .margin, .pager, .footer, .stepper-bar, .playground-bar { display: none !important; }
  .shell, .main, .layout { display: block; padding: 0; max-width: none; }
  .content { max-width: none; }
  html { background: #fff; color: #000; font-size: 11pt; }
  .reveal { opacity: 1 !important; transform: none !important; }
  .stepper .step[hidden] { display: block !important; }
  .print-chapter { break-before: page; border: 0; }
  a { color: inherit; }
  .codeblock, .playground, .goal, .playground-editor, .theorem, .definition, .exercise, .rulebox, .stepper { box-shadow: none; border-color: #bbb; background: #f6f6f6; color: #000; }
  .hero .playground { transform: none; }
}

/* ---------- Explorers (explorers.js) ---------- */

.explorer {
  margin: 1.6rem 0 1.9rem;
  background: var(--bg2);
  border: 1px solid var(--border);
  border-radius: var(--r);
  overflow: hidden;
  box-shadow: var(--shadow-sm);
}
.explorer > pre.prelude, .explorer > pre.script { display: none; }
.ex-bar {
  display: flex; align-items: center; gap: .6rem;
  padding: .55rem .9rem;
  background: var(--bg3);
  border-bottom: 1px solid var(--border);
}
.ex-title { font: 500 .76rem var(--mono); letter-spacing: .08em; color: var(--accent); margin-right: auto; }
.ex-status { font: .72rem var(--mono); color: var(--muted); }
.ex-inputs {
  display: flex; flex-wrap: wrap; gap: .5rem .8rem; align-items: flex-end;
  padding: .7rem .9rem;
  border-bottom: 1px solid var(--border);
  margin: 0;
}
.ex-field { display: flex; flex-direction: column; gap: .2rem; flex: 1 1 10rem; min-width: 0; }
.ex-field.wide { flex: 3 1 22rem; }
.ex-label { font: .66rem var(--mono); letter-spacing: .08em; text-transform: uppercase; color: var(--dim); }
.ex-input {
  font: 400 .84rem var(--mono);
  color: var(--fg);
  background: var(--well);
  border: 1px solid var(--border);
  border-radius: 6px;
  padding: .45rem .6rem;
  width: 100%;
  min-width: 0;
}
.ex-input:focus { outline: none; border-color: var(--accent); }
select.ex-input { cursor: pointer; }
.ex-go {
  font: 700 .76rem var(--mono);
  color: var(--accent-ink);
  background: var(--accent-solid);
  border: 1px solid var(--accent-solid);
  border-radius: 999px;
  padding: .45rem .95rem;
  cursor: pointer;
  align-self: flex-end;
}
.ex-go:hover { filter: brightness(1.08); }
.ex-body { padding: .9rem .9rem .4rem; }
.ex-error { padding: .6rem .9rem .8rem; font: .8rem/1.5 var(--mono); color: var(--bad); white-space: pre-wrap; }
.ex-verdict { margin: .6rem 0 .6rem; font: .8rem/1.5 var(--mono); color: var(--ok); }
.ex-verdict.bad { color: var(--bad); }
.ex-hint, .ex-picked { font: .76rem/1.5 var(--mono); color: var(--muted); margin: .5rem 0 .4rem; }
.ex-modes { display: flex; gap: .4rem; margin-bottom: .7rem; }

/* Tokens */
.tokens, .ex-term {
  font: .84rem/1.7 var(--mono);
  white-space: pre-wrap;
  word-break: break-word;
}
.ex-term { margin: 0 0 .7rem; padding: .5rem .7rem; background: var(--well); border: 1px solid var(--border); border-radius: 8px; }
.ex-term.big { font-size: 1rem; }
.tk-kw { color: var(--accent); font-weight: 500; }
.tk-sort { color: var(--fg2); }
.tk-const { color: var(--info); }
.tk-punct { color: var(--muted); }
.tk-free { color: var(--fg); text-decoration: underline dotted var(--muted); text-underline-offset: .2em; }
.tk-binder { font-weight: 700; border-bottom: 2px solid currentColor; }
.tk-bound { font-weight: 500; }
.tk-b0 { color: #7fc8e8; } .tk-b1 { color: #f0b35c; } .tk-b2 { color: #b08ad6; }
.tk-b3 { color: #7db8d3; } .tk-b4 { color: #e58fb3; } .tk-b5 { color: #c9d36b; }
html.light .tk-b0 { color: #1a6f95; } html.light .tk-b1 { color: #b06d00; } html.light .tk-b2 { color: #6f3fb8; }
html.light .tk-b3 { color: #1f6f95; } html.light .tk-b4 { color: #b8336e; } html.light .tk-b5 { color: #6f7a0f; }
.tk-hl { background: rgba(255, 255, 255, .12); border-radius: 3px; outline: 1px solid currentColor; }
html.light .tk-hl { background: rgba(0, 0, 0, .08); }
.tk-hole { color: var(--accent); background: rgba(31, 157, 85, .14); border: 1px dashed var(--accent-soft); border-radius: 4px; padding: 0 .15em; }
.tk-hole.tk-current { background: var(--accent-solid); color: var(--accent-ink); border-style: solid; }
.tk-mark { background: rgba(31, 157, 85, .16); box-shadow: 0 0 0 1px rgba(31, 157, 85, .5); border-radius: 3px; padding: 0 .1em; box-decoration-break: clone; -webkit-box-decoration-break: clone; }
html.light .tk-mark { background: rgba(29, 127, 70, .12); }

/* ast */
ul.ast, ul.ast ul { list-style: none; margin: 0; padding-left: 1.4rem; position: relative; }
ul.ast { padding-left: 0; margin: .4rem 0 .6rem; }
ul.ast ul { border-left: 1px solid var(--border2); margin-left: .5rem; }
ul.ast li { position: relative; margin: .2rem 0; }
ul.ast ul > li::before { content: ""; position: absolute; left: -1.4rem; top: .95em; width: .9rem; border-top: 1px solid var(--border2); }
.ast-head { display: inline-flex; gap: .45rem; align-items: baseline; padding: .15rem .5rem; border-radius: 6px; border: 1px solid transparent; cursor: pointer; font: .82rem var(--mono); }
.ast-head:hover, .ast-head.on { border-color: var(--accent-soft); background: var(--well); }
.ast-kind { font-weight: 700; }
.ast-Sort .ast-kind { color: var(--fg2); } .ast-Var .ast-kind { color: #7fc8e8; } .ast-Const .ast-kind { color: var(--info); }
.ast-Pi .ast-kind { color: var(--accent); } .ast-Lam .ast-kind { color: #f0b35c; } .ast-App .ast-kind { color: #b08ad6; }
.ast-label { color: var(--fg); }

/* derivation: list view */
.dv-list { font-size: .84rem; }
.dv-row { display: flex; flex-wrap: wrap; align-items: baseline; gap: .35rem .5rem; }
.dv-premise { font: .66rem var(--mono); letter-spacing: .04em; color: var(--dim); }
.dv-judgment { font: .84rem var(--mono); }
.dv-ctx { color: var(--muted); }
.dv-turnstile { color: var(--accent); font-weight: 700; }
.dv-term { color: var(--fg); }
.dv-type { color: #a9bdd0; }
html.light .dv-type { color: #2f5f8c; }
.dv-fail { color: var(--bad); }
.dv-rule { font: 500 .66rem var(--mono); letter-spacing: .08em; color: var(--accent); border: 1px solid var(--accent-soft); border-radius: 999px; padding: .05rem .45rem; }
.dv-note { font: .74rem/1.5 var(--mono); color: var(--muted); margin: .15rem 0 .2rem 1.2rem; }
.dv-item.fail > .dv-row .dv-rule { border-color: var(--bad); color: var(--bad); }

/* derivation: proof-tree view */
.dv-scroll { overflow-x: auto; padding: .6rem .2rem 1rem; }
.dv-node { display: inline-flex; flex-direction: column; align-items: center; margin: 0 .6rem; font: .78rem var(--mono); }
.dv-premises { display: flex; align-items: flex-end; gap: 3rem; margin-bottom: .25rem; }
.dv-line { position: relative; width: 100%; border-top: 1px solid var(--fg2); margin: .15rem 0; }
.dv-line .dv-rule { position: absolute; left: 100%; top: -.7em; margin-left: .35rem; white-space: nowrap; background: var(--bg2); }
.dv-conclusion { white-space: nowrap; padding: 0 .2rem; }
.dv-node.fail > .dv-line { border-top-color: var(--bad); }

/* reduction */
.rd-steps { list-style: none; margin: 0 0 .8rem; padding: 0; }
.rd-step { padding: .55rem 0 .4rem; border-bottom: 1px dashed var(--border); }
.rd-head { display: flex; align-items: baseline; gap: .6rem; margin-bottom: .3rem; }
.rd-kind { font: 700 .8rem var(--mono); color: var(--accent); min-width: 2.4rem; }
.rd-what { font: .74rem var(--mono); color: var(--muted); }
.rd-before, .rd-after { font: .82rem/1.65 var(--mono); white-space: pre-wrap; word-break: break-word; }
.rd-arrow { color: var(--dim); font: .8rem var(--mono); padding: .1rem 0 .1rem .4rem; }
.rd-none { font: .8rem var(--mono); color: var(--muted); }
.rd-result { padding-top: .3rem; }
.rd-line { display: flex; flex-direction: column; gap: .2rem; margin-bottom: .6rem; font: .82rem/1.6 var(--mono); }
.rd-label { font: .66rem var(--mono); letter-spacing: .08em; text-transform: uppercase; color: var(--dim); }
.rd-stuck { font: .76rem/1.5 var(--mono); color: var(--accent); margin: -.3rem 0 .6rem; }
.rd-dim { color: var(--muted); font-size: .76rem; }

/* scope and substitution */
.sc-legend { display: grid; grid-template-columns: auto 1fr; gap: .3rem .8rem; align-items: baseline; font: .76rem/1.5 var(--mono); color: var(--muted); margin: .2rem 0 .5rem; }
.sc-key { justify-self: start; }
.sb-top { display: flex; flex-wrap: wrap; align-items: baseline; gap: .5rem; margin-bottom: .8rem; }
.sb-top .ex-term { margin: 0; }
.sb-brackets { font: .9rem var(--mono); color: var(--fg2); }
.sb-cols { display: grid; grid-template-columns: 1fr 1fr; gap: .8rem; }
.sb-col { border: 1px solid var(--border); border-radius: 8px; padding: .6rem .7rem .4rem; }
.sb-col.bad { border-color: var(--bad); }
.sb-col.ok { border-color: var(--ok); }
.sb-h { font: 500 .68rem var(--mono); letter-spacing: .08em; text-transform: uppercase; color: var(--muted); margin-bottom: .4rem; }
.sb-col.bad .sb-h { color: var(--bad); } .sb-col.ok .sb-h { color: var(--ok); }
.sb-note { font: .74rem/1.5 var(--mono); color: var(--muted); }
@media (max-width: 700px) { .sb-cols { grid-template-columns: 1fr; } }

/* proof explorer */
.pf-editor { padding: .7rem .9rem; border-bottom: 1px solid var(--border); background: var(--well); }
.pf-textarea { display: block; width: 100%; font: .82rem/1.55 var(--mono); color: var(--fg); background: transparent; border: 1px solid var(--border); border-radius: 6px; padding: .6rem .7rem; margin-bottom: .5rem; resize: vertical; }
.pf-textarea:focus { outline: none; border-color: var(--accent); }
.pf-panels { display: grid; grid-template-columns: minmax(10rem, .8fr) minmax(12rem, 1fr) minmax(12rem, 1.1fr); gap: 0; }
.pf-panel { padding: .8rem .9rem .9rem; border-right: 1px solid var(--border); min-width: 0; }
.pf-panel:last-child { border-right: 0; }
.pf-h { font: .66rem var(--mono); letter-spacing: .1em; text-transform: uppercase; color: var(--dim); margin-bottom: .5rem; }
.pf-line { font: .8rem/1.5 var(--mono); padding: .15rem .45rem; border-radius: 4px; cursor: pointer; color: var(--muted); white-space: pre-wrap; word-break: break-word; border-left: 2px solid transparent; }
.pf-line.done { color: var(--fg2); }
.pf-line.on { background: var(--well); color: var(--fg); border-left-color: var(--accent); }
.pf-line.bad { color: var(--bad); }
.pf-line .k { color: var(--accent); font-weight: 500; }
.pf-line .c { color: var(--dim); }
.pf-line .n { color: var(--info); }
.pf-line:hover { color: var(--fg); }
.pf-goals .goals { margin: 0; }
.pf-goals .goal.current { border-color: var(--accent-soft); }
.pf-term .ex-term { margin-bottom: .4rem; }
.pf-checked { color: var(--ok); }
.pf-sub, .pf-note { font: .72rem/1.5 var(--mono); color: var(--muted); }
.pf-error { font: .8rem/1.5 var(--mono); color: var(--bad); white-space: pre-wrap; }
.pf-qed { font: .82rem/1.5 var(--mono); color: var(--ok); }
.pf-nav { border-top: 1px solid var(--border); border-bottom: 0; }
.pf-note { margin-left: auto; }
@media (max-width: 900px) { .pf-panels { grid-template-columns: 1fr; } .pf-panel { border-right: 0; border-bottom: 1px solid var(--border); } }

/* constructor tree */
.ct-tree { margin: .3rem 0 .6rem; }
.ct-node { border: 1px solid var(--border2); border-radius: 8px; padding: .5rem .7rem .45rem; background: var(--well); display: inline-block; max-width: 100%; }
.ct-head { display: flex; flex-wrap: wrap; align-items: baseline; gap: .4rem; font: .82rem var(--mono); }
.ct-ctor { color: var(--info); font-weight: 700; }
.ct-param { color: var(--muted); }
.ct-field { color: var(--fg2); background: var(--bg2); border: 1px solid var(--border); border-radius: 4px; padding: 0 .35rem; font-size: .76rem; }
.ct-children { display: flex; flex-wrap: wrap; gap: .7rem; margin: .5rem 0 .2rem; padding-left: .9rem; border-left: 2px solid var(--border2); }
.ct-slot-label { font: .64rem var(--mono); letter-spacing: .06em; color: var(--dim); margin-bottom: .25rem; }
.ct-leaf { font: .82rem var(--mono); color: var(--fg2); }
.ct-case { font: .72rem var(--mono); color: var(--accent); margin-top: .45rem; }

/* universes */
.un-body { padding-bottom: .9rem; }
.un-controls { display: flex; gap: 1rem; margin-bottom: .8rem; }
.un-controls .ex-field { flex: 0 1 12rem; }
.un-ladder { display: flex; flex-direction: column; gap: .3rem; margin: .4rem 0 .8rem; }
.un-rung { display: flex; align-items: center; gap: .8rem; padding: .4rem .7rem; border: 1px solid var(--border); border-radius: 6px; font: .82rem var(--mono); color: var(--muted); background: var(--well); }
.un-rung.u, .un-rung.v { color: var(--fg); border-color: var(--border2); }
.un-rung.result { border-color: var(--accent); color: var(--fg); box-shadow: 0 0 0 1px var(--accent-soft); }
.un-tags { margin-left: auto; display: flex; gap: .4rem; }
.un-tag { font-size: .7rem; border: 1px solid var(--border2); border-radius: 999px; padding: 0 .45rem; color: var(--fg2); }
.un-tag.hot { border-color: var(--accent); color: var(--accent); }
.un-verdict { font: .8rem/1.6 var(--mono); color: var(--fg2); }

/* long implementation listings fold away */
details.code-details > summary { margin-bottom: .3rem; }
details.code-details[open] > summary { margin-bottom: .6rem; }
details.code-details > .codeblock { margin-left: 0; }

/* dependency diagram (Chapter 14) */
.dep-diagram { width: 100%; height: auto; display: block; font: .78rem var(--mono); color: var(--fg2); margin: .4rem 0 .6rem; }
.dep-box rect { fill: var(--bg2); stroke: var(--border2); }
.dep-box text { fill: var(--fg); }
.dep-box.hot rect { stroke: var(--accent); }
.dep-box.hot text { fill: var(--accent); }
.dep-box.goal rect { fill: var(--well); stroke: var(--ok); }
.dep-box.goal text { fill: var(--ok); font-weight: 700; }
.dep-arrows path { fill: none; stroke: var(--muted); stroke-width: 1.2; marker-end: url(#arr); }

/* ---------- Languages ---------- */

.langs { display: flex; gap: .15rem; align-items: center; margin-right: .4rem; font: 500 .74rem var(--mono); }
.langs .lang { color: var(--muted); border: 0; padding: .3rem .5rem; border-radius: 999px; }
.langs a.lang:hover { color: var(--accent); }
.langs .lang.current { color: var(--fg); background: var(--bg2); border: 1px solid var(--border); }

html[lang="ja"] {
  --sans: "IBM Plex Sans", "Hiragino Sans", "Hiragino Kaku Gothic ProN", "Yu Gothic UI", "Yu Gothic", "Meiryo", "Noto Sans JP", "Noto Sans CJK JP", -apple-system, system-ui, sans-serif;
  --mono: "IBM Plex Mono", "SF Mono", ui-monospace, Menlo, Consolas, "Noto Sans Mono CJK JP", monospace;
}
html[lang="zh-Hans"] {
  --sans: "IBM Plex Sans", "PingFang SC", "Hiragino Sans GB", "Microsoft YaHei", "Noto Sans SC", "Noto Sans CJK SC", -apple-system, system-ui, sans-serif;
  --mono: "IBM Plex Mono", "SF Mono", ui-monospace, Menlo, Consolas, "Noto Sans Mono CJK SC", monospace;
}
html[lang="ja"] body, html[lang="zh-Hans"] body { line-height: 1.85; }
html[lang="ja"] h1, html[lang="zh-Hans"] h1 { letter-spacing: 0; line-height: 1.3; }
html[lang="ja"] h2, html[lang="zh-Hans"] h2 { letter-spacing: 0; line-height: 1.35; }
html[lang="ja"] .chapter-label, html[lang="zh-Hans"] .chapter-label { letter-spacing: .06em; text-transform: none; }
html[lang="ja"] .lead, html[lang="zh-Hans"] .lead { line-height: 1.9; }

/* Callout labels per language (the English labels are set earlier). */
html[lang="ja"] aside.note::before { content: "注"; }
html[lang="ja"] aside.intuition::before { content: "直観"; }
html[lang="ja"] aside.history::before { content: "背景"; }
html[lang="ja"] aside.lean::before { content: "Lean 4 では"; }
html[lang="ja"] aside.code::before { content: "コードでは"; }
html[lang="ja"] aside.warning::before { content: "落とし穴"; }
html[lang="ja"] .proof > p:first-child::before { content: "証明. "; }
html[lang="ja"] .exercise > p:first-child::before { content: "演習 "; }
html[lang="zh-Hans"] aside.note::before { content: "注"; }
html[lang="zh-Hans"] aside.intuition::before { content: "直觉"; }
html[lang="zh-Hans"] aside.history::before { content: "背景"; }
html[lang="zh-Hans"] aside.lean::before { content: "在 Lean 4 中"; }
html[lang="zh-Hans"] aside.code::before { content: "代码中"; }
html[lang="zh-Hans"] aside.warning::before { content: "陷阱"; }
html[lang="zh-Hans"] .proof > p:first-child::before { content: "证明. "; }
html[lang="zh-Hans"] .exercise > p:first-child::before { content: "练习 "; }
html[lang="ja"] .summary-box > p:first-child, html[lang="zh-Hans"] .summary-box > p:first-child { text-transform: none; letter-spacing: .08em; }

/* Translation notice (shown only in locales that set one). */
.notice {
  margin: .4rem 0 1.6rem;
  padding: .6rem .9rem;
  border: 1px solid var(--border2);
  border-left: 3px solid var(--warn);
  border-radius: var(--r);
  background: var(--bg2);
  font-size: .86rem;
  line-height: 1.7;
  color: var(--fg2);
}
.page-print .notice { margin-bottom: 2rem; }
.topbar-h5i { color: #ff6258; font-weight: 700; }
.topbar-h5i:hover { color: #ff6258; border-color: #e0241b; }