/* Part of the Grace17 proof assistant for mathematics based on set theory.
   Copyright (c) 2026 Grant Passmore.
   Released under the Apache License 2.0. See LICENSE in the repository root.
   Authors: Grant Passmore */

:root {
  --header-height: 3.6rem;
  color-scheme: dark;
  --navy: #12233f;
  --cream: #f2ecdd;
  --verdigris: #55b39e;
  --verdigris-bright: #71d8c0;
  --slate: #8ea3c4;
  --brace: #182b4a;
  --ink: #0c1b30;
  --line: #27405f;
  --line-strong: #3b5579;
  --kw: #57f4ff;
  --tactic: #65aef2;
  --type: #00c8d7;
  --number: #8bbef0;
  --operator: #aab8c0;
  --connective: #65aef2;
  --comment: #7f93a8;
  --string: #d9a441;
  --ident: #d8e2e7;
  --mono: "JetBrains Mono", ui-monospace, Menlo, Consolas, monospace;
}
* { box-sizing: border-box; }
html { background: var(--navy); }
body { margin: 0; min-height: 100vh; background: var(--navy); color: var(--cream); font-family: var(--mono); font-size: 15px; line-height: 1.7; -webkit-font-smoothing: antialiased; }
a { color: var(--verdigris); text-decoration-thickness: 1px; text-underline-offset: .22em; }
a:hover { color: var(--verdigris-bright); }
a:focus-visible, button:focus-visible, input:focus-visible, summary:focus-visible { outline: 2px solid var(--verdigris-bright); outline-offset: 3px; }
::selection { background: var(--verdigris); color: var(--navy); }

/* Header and footer */
.site-header { display: flex; align-items: center; justify-content: space-between; gap: 1.5rem; padding: .9rem 5%; border-bottom: 1px solid var(--line); background: var(--navy); }
.brand { display: inline-flex; align-items: center; }
.brand svg { width: 118px; height: auto; display: block; }
.site-nav { display: flex; flex-wrap: wrap; gap: .3rem 1.4rem; font-size: .9rem; }
.site-nav a { color: var(--cream); text-decoration: none; padding: .2rem 0; border-bottom: 1px solid transparent; }
.site-nav a:hover, .site-nav a[aria-current="page"] { color: var(--verdigris-bright); border-bottom-color: var(--verdigris); }
.site-footer { margin-top: 4rem; padding: 1.5rem 5%; border-top: 1px solid var(--line); color: var(--slate); font-size: .8rem; display: flex; flex-wrap: wrap; gap: .5rem 2rem; }

/* Layout */
.layout { max-width: 1180px; margin: 0 auto; padding: 2rem 1.5rem 3rem; display: grid; grid-template-columns: minmax(0, 1fr); gap: 2.5rem; }
.layout.with-sidebar { grid-template-columns: 250px minmax(0, 1fr); }
main.doc { max-width: 78ch; min-width: 0; }
main.wide { max-width: none; }
.sidebar { font-size: .82rem; }
.sidebar details { position: sticky; top: calc(var(--header-height) + 1rem); max-height: calc(100vh - var(--header-height) - 2rem); overflow-y: auto; overscroll-behavior: contain; padding-right: .4rem; scrollbar-width: thin; scrollbar-color: var(--line-strong) transparent; }
.sidebar details::-webkit-scrollbar { width: 6px; }
.sidebar details::-webkit-scrollbar-thumb { background: var(--line-strong); border-radius: 3px; }
.sidebar summary { cursor: pointer; color: var(--slate); text-transform: uppercase; letter-spacing: .08em; font-size: .72rem; margin-bottom: .6rem; }
.sidebar h3 { margin: 1.1rem 0 .3rem; font-size: .72rem; font-weight: 500; text-transform: uppercase; letter-spacing: .08em; color: var(--slate); }
.sidebar ul { list-style: none; margin: 0; padding: 0; }
.sidebar li { margin: 0; }
.sidebar a { display: block; color: var(--cream); text-decoration: none; padding: .18rem .5rem; border-left: 2px solid transparent; margin-left: -.5rem; }
.sidebar a:hover { color: var(--verdigris-bright); }
.sidebar a[aria-current="page"] { color: var(--verdigris-bright); border-left-color: var(--verdigris); }

/* Typography */
h1, h2, h3, h4 { font-weight: 500; line-height: 1.25; overflow-wrap: anywhere; }
h1 { font-size: clamp(1.6rem, 3vw, 2.1rem); margin: 0 0 1.2rem; }
h2 { font-size: 1.3rem; margin: 2.4rem 0 .8rem; padding-bottom: .3rem; border-bottom: 1px solid var(--line); }
h3 { font-size: 1.05rem; margin: 1.8rem 0 .6rem; color: var(--verdigris-bright); }
h4 { font-size: .95rem; margin: 1.4rem 0 .5rem; }
.anchor { margin-left: .45em; color: var(--slate); text-decoration: none; opacity: 0; font-weight: 400; }
h2:hover .anchor, h3:hover .anchor, h4:hover .anchor, .anchor:focus { opacity: 1; }
p, ul, ol, table, blockquote { margin: 0 0 1.1rem; }
li { margin: .25rem 0; overflow-wrap: anywhere; }
li > ul, li > ol { margin-bottom: .2rem; }
strong { font-weight: 500; color: #fff8e8; }
hr { border: 0; border-top: 1px solid var(--line); margin: 2.5rem 0; }
blockquote { border-left: 3px solid var(--verdigris); margin-left: 0; padding: .2rem 0 .2rem 1.1rem; color: var(--slate); }
blockquote p:last-child { margin-bottom: 0; }
small, .muted { color: var(--slate); }
code { font-family: var(--mono); font-size: .92em; }
:not(pre) > code { background: var(--brace); color: var(--ident); padding: .08em .38em; border-radius: 4px; }
table { border-collapse: collapse; width: 100%; font-size: .9rem; display: block; overflow-x: auto; }
th, td { border: 1px solid var(--line); padding: .5rem .7rem; text-align: left; vertical-align: top; }
th { background: var(--brace); font-weight: 500; }
details { margin: 0 0 1.1rem; }
summary { cursor: pointer; }
kbd { font-family: var(--mono); border: 1px solid var(--line-strong); border-radius: 4px; padding: 0 .3em; font-size: .85em; }

/* Code blocks */
figure.code { margin: 1.3rem 0; border: 1px solid var(--line); border-radius: 8px; background: var(--ink); overflow: hidden; }
.code-bar { display: flex; align-items: center; gap: .5rem; padding: .35rem .6rem .35rem .9rem; background: var(--brace); border-bottom: 1px solid var(--line); }
.code-lang { font-size: .7rem; letter-spacing: .08em; text-transform: uppercase; color: var(--slate); }
.code-spacer { flex: 1; }
.action { font: inherit; font-size: .74rem; line-height: 1; color: var(--verdigris-bright); background: transparent; border: 1px solid var(--line-strong); border-radius: 6px; padding: .35rem .6rem; text-decoration: none; cursor: pointer; white-space: nowrap; }
.action:hover { background: var(--verdigris); border-color: var(--verdigris); color: var(--navy); }
.action.run { border-color: var(--verdigris); }
figure.code pre { margin: 0; padding: .9rem 1.1rem; overflow-x: auto; background: transparent; border: 0; border-radius: 0; }
pre { background: var(--ink); border: 1px solid var(--line); border-radius: 8px; padding: .9rem 1.1rem; overflow-x: auto; margin: 0 0 1.1rem; line-height: 1.55; }
pre code { color: var(--ident); font-size: .88rem; }
.g17-keyword { color: var(--kw); }
.g17-tactic { color: var(--tactic); }
.g17-type { color: var(--type); }
.g17-number { color: var(--number); }
.g17-operator { color: var(--operator); }
.g17-connective { color: var(--connective); }
.g17-comment { color: var(--comment); font-style: italic; }
.g17-string { color: var(--string); }

/* Source pages */
.source-meta { color: var(--slate); font-size: .88rem; margin-bottom: 1.2rem; }
.source-meta a { margin-right: 1rem; }
.declarations { columns: 2; column-gap: 2rem; font-size: .88rem; }
.declarations li { break-inside: avoid; }
.source { font-size: .88rem; line-height: 1.55; counter-reset: line; }
.source-line { display: block; min-height: 1.55em; scroll-margin-top: 1rem; white-space: pre; }
.source-line:target { background: #1f3f4f; }
.line-number { display: inline-block; width: 3.6rem; color: #53646e; text-decoration: none; user-select: none; }
.line-number:hover { color: var(--slate); }

/* Search and result cards */
input[type="search"], input[type="text"] { display: block; width: 100%; font: inherit; padding: .8rem 1rem; background: var(--ink); color: var(--cream); border: 1px solid var(--line-strong); border-radius: 8px; }
input::placeholder { color: var(--slate); }
.result { border: 1px solid var(--line); border-radius: 8px; padding: .9rem 1.1rem; margin: .8rem 0; background: var(--brace); }
.result .result-head { display: flex; flex-wrap: wrap; gap: .3rem 1.2rem; align-items: baseline; margin-bottom: .5rem; }
.result pre { white-space: pre-wrap; margin: 0; background: var(--ink); }
.module-tree { columns: 2; column-gap: 2rem; font-size: .88rem; list-style: none; padding: 0; }
.module-tree li { break-inside: avoid; }
.module-tree small, .module-section h2 small, .area-nav small { color: var(--slate); font-weight: 400; font-size: .8em; }
.module-section { margin-top: 2.2rem; }
.module-section h2 { margin-bottom: .2rem; }
.module-section p.muted { margin-top: 0; }
.area-nav { display: flex; flex-wrap: wrap; gap: .4rem .9rem; list-style: none; padding: 0; margin: .4rem 0 1rem; font-size: .9rem; }
.card-grid { display: grid; grid-template-columns: repeat(auto-fill, minmax(260px, 1fr)); gap: 1rem; list-style: none; padding: 0; }
.card { border: 1px solid var(--line); border-radius: 8px; padding: .9rem 1.1rem; background: var(--brace); }
.card a { text-decoration: none; }
.card p { margin: .3rem 0 0; color: var(--slate); font-size: .85rem; }
.proof-frame { width: 100%; height: 80vh; min-height: 500px; border: 1px solid var(--line); border-radius: 8px; }
.lede { font-size: 1.05rem; color: var(--slate); }

@media (max-width: 860px) {
  .layout.with-sidebar { grid-template-columns: minmax(0, 1fr); gap: 1.5rem; }
  .sidebar details { position: static; max-height: none; overflow: visible; }
  .sidebar summary::after { content: " ▾"; }
  .declarations, .module-tree { columns: 1; }
}
@media (min-width: 861px) {
  /* The header stays put and the documentation sidebar sits under it, so
     following a link changes the page without moving the sidebar. */
  .site-header { position: sticky; top: 0; z-index: 5; }
  [id] { scroll-margin-top: calc(var(--header-height) + 1rem); }
  .sidebar summary { list-style: none; pointer-events: none; }
  .sidebar summary::-webkit-details-marker { display: none; }
}
@media (max-width: 650px) {
  .site-header { flex-direction: column; align-items: flex-start; gap: .6rem; padding: .9rem 1rem; }
  .layout { padding: 1.2rem 1rem 2rem; }
  .line-number { width: 2.6rem; }
}

/* Illustrations from docs/images. */
figure.illustration { margin: 1.6rem auto; max-width: 100%; text-align: center; }
figure.illustration img { display: block; margin: 0 auto; max-width: 100%; max-height: 420px; width: auto; height: auto; }
figure.illustration figcaption { margin-top: .5rem; color: var(--slate); font-size: .85rem; }

/* Inline code that names a library declaration. */
a.decl { color: inherit; text-decoration: none; border-bottom: 1px dotted var(--verdigris); }
a.decl:hover, a.decl:focus-visible { color: var(--verdigris-bright); border-bottom-style: solid; outline: none; }
.decl-card { position: fixed; z-index: 30; padding: .6rem .8rem; border: 1px solid var(--line-strong); border-radius: 0; background: var(--ink); color: var(--cream); box-shadow: 0 10px 30px rgba(0,0,0,.45); pointer-events: none; }
.decl-card-head { margin-bottom: .4rem; font-size: .78rem; color: var(--slate); overflow-wrap: anywhere; }
.decl-card pre { margin: 0; padding: 0; border: 0; background: transparent; white-space: pre-wrap; font-size: .82rem; line-height: 1.5; }
.decl-card small { display: block; margin-top: .4rem; color: var(--slate); font-size: .72rem; }
.note { border-bottom: 1px dotted var(--verdigris); cursor: help; }
.note:hover, .note:focus-visible { color: var(--verdigris-bright); border-bottom-style: solid; outline: none; }
.decl-card-note { margin: 0; font-size: .88rem; line-height: 1.5; }

/* A profile link: a dotted underline, a hover card with the photo and name,
   and the click goes to the person's page. */
a.profile { color: inherit; text-decoration: underline dotted var(--verdigris); text-underline-offset: .18em; }
a.profile:hover, a.profile:focus-visible { color: var(--verdigris-bright); text-decoration-style: solid; outline: none; }
.byline { display: flex; align-items: center; gap: .9rem; margin: -.4rem 0 1.4rem; font-size: .95rem; line-height: 1.35; }
.byline img { width: 60px; height: 60px; border-radius: 50%; object-fit: cover; box-shadow: 0 0 0 2px var(--verdigris), 0 6px 18px rgba(0, 0, 0, .35); flex: none; }
.byline time { opacity: .72; }
.preface { font-style: italic; background: var(--brace); border-left: 3px solid var(--verdigris); border-radius: 0 8px 8px 0; padding: .95rem 1.25rem; margin: 1.6rem 0; color: var(--cream); }
.preface p { margin: 0; }
.preface a { font-style: normal; }
.section-mark { display: flex; justify-content: center; align-items: center; gap: 1rem; width: 100%; margin: 2.2rem 0 1.8rem; color: var(--verdigris); text-align: center; }
.section-mark::before, .section-mark::after { content: ""; display: block; width: 7rem; max-width: 30%; height: 1px; background: linear-gradient(90deg, transparent, var(--line-strong)); }
.section-mark::after { background: linear-gradient(90deg, var(--line-strong), transparent); }
.section-mark span { display: inline-block; font-family: Georgia, "Times New Roman", serif; font-size: 1.7rem; line-height: 1; text-shadow: 0 0 14px rgba(85, 179, 158, .55); }
.decl-card-profile { display: flex; align-items: center; gap: .7rem; }
.decl-card-profile img { width: 3.4rem; height: 3.4rem; border-radius: 50%; object-fit: cover; flex: none; }
.decl-card-profile strong { display: block; font-weight: 500; color: var(--cream); font-size: .92rem; }
.decl-card-profile small { display: block; margin-top: .15rem; color: var(--slate); font-size: .72rem; }

/* Breadcrumbs on module pages lead back up the library hierarchy. */
.breadcrumbs { font-size: .8rem; color: var(--slate); margin: 0 0 .8rem; display: flex; flex-wrap: wrap; gap: .35rem; align-items: center; }
.breadcrumbs a { color: var(--slate); text-decoration: none; }
.breadcrumbs a:hover { color: var(--verdigris-bright); text-decoration: underline; }
.breadcrumbs [aria-current="page"] { color: var(--cream); }
.breadcrumbs .sep { opacity: .6; }

/* Natural-deduction derivations rendered from checked kernel proofs. */
.nd-figure { margin: 1.2rem 0; border: 1px solid var(--line); border-radius: 6px; background: var(--ink); padding: .6rem .8rem; }
.nd-caption { font-size: .78rem; color: var(--slate); margin-bottom: .5rem; }
.nd-view-title { font-size: .7rem; text-transform: uppercase; letter-spacing: .08em; color: var(--slate); margin: .6rem 0 .3rem; }
.fitch-proof { border-top: 1px solid var(--line-strong); font-size: .78rem; }
.fitch-line > summary { display: grid; grid-template-columns: 2.4rem minmax(0, 1fr) minmax(7rem, .32fr); align-items: stretch; min-height: 1.9rem; cursor: pointer; list-style: none; border-bottom: 1px solid var(--line); }
.fitch-line > summary::-webkit-details-marker { display: none; }
.fitch-line > summary:hover, .fitch-line:target > summary { background: var(--brace); }
.fitch-number { padding: .45rem .45rem .4rem 0; color: var(--slate); text-align: right; font-size: .7rem; user-select: none; }
.fitch-formula { min-width: 0; display: flex; align-items: stretch; }
.fitch-rails { flex: 0 0 auto; display: flex; }
.fitch-rail { display: block; width: .8rem; border-left: 1px solid var(--line-strong); }
.fitch-formula > code { min-width: 0; padding: .4rem .5rem .35rem .3rem; color: var(--cream); overflow-wrap: anywhere; background: none; }
.fitch-line.scope-start .fitch-formula > code { border-top: 1px solid var(--verdigris); }
.fitch-line.assumption .fitch-formula > code { color: #fff; }
.fitch-justification { min-width: 0; display: flex; justify-content: flex-end; align-items: baseline; gap: .5rem; padding: .4rem .2rem .35rem .5rem; text-align: right; }
.fitch-justification strong { color: var(--kw); font-weight: 500; white-space: nowrap; }
.fitch-justification strong a { color: var(--tactic); text-decoration: none; }
.fitch-justification small { overflow: hidden; color: var(--slate); font-size: .68rem; text-overflow: ellipsis; white-space: nowrap; }
.fitch-detail { margin-left: calc(2.4rem + var(--fitch-depth) * .8rem); padding: .5rem .6rem .6rem; border-bottom: 1px solid var(--line-strong); border-left: 2px solid var(--verdigris); background: var(--navy); }
.nd-inference { display: grid; grid-template-columns: minmax(0, 1fr) minmax(8rem, .3fr); gap: 1rem; align-items: center; padding: .5rem; }
.nd-rule { min-width: 0; display: flex; flex-direction: column; }
.nd-premises { min-height: .5rem; display: flex; justify-content: space-around; align-items: flex-end; gap: 1rem; }
.nd-premise { min-width: 0; flex: 1 1 0; display: flex; flex-direction: column; align-items: center; gap: .2rem; text-align: center; }
.nd-premise > code { color: var(--cream); overflow-wrap: anywhere; background: none; }
.nd-premise > span { color: var(--slate); font-size: .66rem; }
.nd-discharged { display: flex; flex-wrap: wrap; justify-content: center; gap: .3rem; }
.nd-discharged code, .gz-discharged { color: var(--tactic); font-size: .7rem; background: none; }
.nd-rule-bar { display: grid; grid-template-columns: minmax(0, 1fr) auto; gap: .5rem; align-items: end; margin-top: .3rem; }
.nd-rule-bar span { height: 1px; background: var(--cream); }
.nd-rule-bar strong { color: var(--kw); font-weight: 500; font-size: .75rem; }
.nd-conclusion { align-self: center; padding: .4rem .5rem 0; color: #fff; text-align: center; overflow-wrap: anywhere; background: none; }
.nd-rule-aside { min-width: 0; align-self: stretch; padding: .3rem 0 .3rem .8rem; border-left: 1px solid var(--line-strong); }
.nd-rule-aside > strong { display: block; color: var(--cream); font-weight: 500; font-size: .75rem; }
.nd-side-conditions { margin-top: .5rem; }
.nd-side-conditions span { display: block; color: var(--slate); font-size: .66rem; }
.nd-side-conditions code { display: block; color: var(--string); font-size: .7rem; background: none; }
.fitch-arguments { margin: .5rem 0 0; }
.fitch-arguments div { display: grid; grid-template-columns: minmax(6rem, .28fr) minmax(0, 1fr); gap: .5rem; }
.fitch-arguments dt { color: var(--slate); font-size: .7rem; }
.fitch-arguments dd { margin: 0; color: var(--cream); font-size: .72rem; overflow-wrap: anywhere; }
.gentzen-proof { overflow-x: auto; padding: .6rem .4rem; font-size: .76rem; }
.gz-node { display: inline-flex; flex-direction: column; align-items: center; vertical-align: bottom; }
.gz-premises { display: flex; align-items: flex-end; justify-content: center; gap: 1.4rem; }
.gz-rule { display: flex; align-items: flex-start; align-self: stretch; }
.gz-concl { flex: 1; border-top: 1px solid var(--cream); padding: .15rem .5rem 0; text-align: center; white-space: nowrap; color: var(--cream); }
.gz-label { font-size: .66rem; color: var(--kw); margin: -.55rem 0 0 .25rem; white-space: nowrap; }
.gz-leaf { padding: 0 .3rem; white-space: nowrap; }
.gz-leaf .gz-formula { color: var(--cream); }
.gz-leaf .gz-label { margin: 0 0 0 .3rem; }
.gz-elided { color: var(--slate); }
.proof-link { font-size: .72rem; color: var(--slate); margin-left: .3rem; }

/* Tactic reference: one collapsible section per tactic. */
details.tactic { border-top: 1px solid var(--line); padding: .2rem 0; }
details.tactic > summary { cursor: pointer; list-style: none; display: flex; align-items: baseline; gap: .5rem; }
details.tactic > summary::-webkit-details-marker { display: none; }
details.tactic > summary::before { content: "▸"; color: var(--slate); font-size: .8rem; }
details.tactic[open] > summary::before { content: "▾"; }
details.tactic > summary h3 { margin: .4rem 0; font-size: 1rem; }
.tactic-body { padding: 0 0 .6rem 1.1rem; }