:root {
  --bg: #fbfaf7;
  --panel: #ffffff;
  --ink: #1d2433;
  --muted: #5f6878;
  --line: #e3e0d8;
  --accent: #335c99;
  --accent-soft: #e6edf7;
  --link: #335c99;
  --menu: #982906;
  --menu-on: #be5100;
  --c-follows: #2f7d4f;
  --c-follows-bg: #e5f3ea;
  --c-indep: #4f7fc0;
  --c-indep-bg: #e9f0fa;
  --c-cons: #6a3d9a;
  --c-cons-bg: #f2ecf9;
  --c-notder: #9a7b3a;
  --c-notder-bg: #f7f0e1;
  --c-open: #9aa0a9;
  --c-open-bg: #f3f3f2;
  --c-refuted: #c0392b;
  --c-refuted-bg: #fbe8e6;
  --serif: "Source Serif 4", Georgia, serif;
  --sans: "Inter", system-ui, -apple-system, sans-serif;
}
@media (prefers-color-scheme: dark) {
  :root:not([data-theme="light"]) {
    --bg: #14171d; --panel: #1b1f27; --ink: #e6e8ec; --muted: #9aa3b2; --line: #2c323d;
    --accent: #8fb1e8; --accent-soft: #23304a; --link: #8fb1e8; --menu: #f2a46c; --menu-on: #be5100;
    --c-follows: #5cc185; --c-follows-bg: #1c3326;
    --c-indep: #7fa9e6; --c-indep-bg: #1f2c42;
    --c-cons: #b99be6; --c-cons-bg: #2c2340;
    --c-notder: #d4b16a; --c-notder-bg: #352c1b;
    --c-open: #7d838d; --c-open-bg: #23262c;
    --c-refuted: #ef7366; --c-refuted-bg: #3c2220;
  }
}
:root[data-theme="dark"] {
  --bg: #14171d; --panel: #1b1f27; --ink: #e6e8ec; --muted: #9aa3b2; --line: #2c323d;
  --accent: #8fb1e8; --accent-soft: #23304a; --link: #8fb1e8; --menu: #f2a46c; --menu-on: #be5100;
  --c-follows: #5cc185; --c-follows-bg: #1c3326;
  --c-indep: #7fa9e6; --c-indep-bg: #1f2c42;
  --c-cons: #b99be6; --c-cons-bg: #2c2340;
  --c-notder: #d4b16a; --c-notder-bg: #352c1b;
  --c-open: #7d838d; --c-open-bg: #23262c;
  --c-refuted: #ef7366; --c-refuted-bg: #3c2220;
}

* { box-sizing: border-box; }
html { -webkit-text-size-adjust: 100%; }
body { margin: 0; background: var(--bg); color: var(--ink); font: 15px/1.5 var(--sans); }
a { color: var(--link); }
.leanb, .leanb:visited { color: #fff; }
.wrap { max-width: 1360px; margin: 0 auto; padding: 0 16px; }
button { font: inherit; color: inherit; cursor: pointer; }
button:focus-visible, .node:focus-visible { outline: 2px solid var(--accent); outline-offset: 2px; }
code { font-size: 0.92em; background: var(--accent-soft); padding: 1px 4px; border-radius: 4px; }

header { border-bottom: 1px solid var(--line); background: var(--panel); }
header h1 { font: 400 36px/1.2 Times, "Times New Roman", serif; margin: 18px 0 6px; }
header .sub { margin: 0 0 12px; color: var(--muted); max-width: 80ch; }
/* the top menu, as on isaacwilhelm.com: orange text; the current page and the one under the pointer get an orange block */
.tabs { display: flex; gap: 0; }
.tabs button { background: none; border: 0; border-radius: 0; padding: 10px; color: var(--menu); font: 16px/1.2 Times, "Times New Roman", serif; cursor: pointer; }
.tabs button:hover, .tabs button[aria-selected="true"] { background: var(--menu-on); color: #fff; }
/* the language switch, under the menu */
.langbar { padding: 8px 0 10px; }
.langsw { display: flex; flex-wrap: wrap; align-items: center; gap: 6px; font-size: 13px; }
.langsw span { color: var(--muted); margin-right: 4px; }
.langsw button { border: 1px solid var(--line); background: var(--bg); border-radius: 999px; padding: 3px 12px; font: inherit; color: var(--ink); cursor: pointer; }
.langsw button[aria-pressed="true"] { background: var(--accent); border-color: var(--accent); color: #fff; }
.langsw button:disabled { opacity: 0.45; cursor: not-allowed; }
.langnote { margin: 6px 0 0; font-size: 13px; color: var(--muted); max-width: 110ch; }
/* the Languages page */
.langpage .rules { display: grid; grid-template-columns: 1fr; gap: 2px; margin: 10px 0 14px; }
.langpage .rule { display: flex; align-items: center; gap: 10px; overflow-x: auto; }
.langpage .rname { font-size: 12px; color: var(--muted); min-width: 92px; text-align: right; }
.langpage .center { text-align: center; }
.langpage .consts td, .langpage .langtable td, .langpage .langtable th { padding: 4px 10px; vertical-align: top; }
.langpage .langtable { width: 100%; table-layout: fixed; }
.langpage .langtable th { text-align: left; font-size: 13px; color: var(--muted); font-weight: 600; }
.langpage .langtable th:nth-child(1) { width: 24%; } .langpage .langtable th:nth-child(2) { width: 33%; }
.langpage .refs li { margin-bottom: 4px; }
.langpage .consts { width: auto; table-layout: auto; }
.langpage .consts td:nth-child(1), .langpage .consts td:nth-child(2) { white-space: nowrap; }

main { padding-top: 18px; padding-bottom: 30px; }
.layout { display: grid; grid-template-columns: 284px minmax(0, 1fr) 256px; gap: 20px; align-items: start; }
.sortsel { display: flex; align-items: center; gap: 8px; font-size: 13px; color: var(--muted); margin: 4px 0 2px; }
.sortsel select { flex: 1; min-width: 0; font: inherit; color: var(--ink); background: var(--bg); border: 1px solid var(--line); border-radius: 6px; padding: 3px 6px; }
.msep { display: flex; align-items: center; gap: 6px; font-size: 11px; font-style: italic; color: var(--muted); margin: 3px 4px 1px 40px; }
.msep::before, .msep::after { content: ""; flex: 1; border-top: 1px dashed var(--line); }
.msep::before { flex: 0 0 6px; }
.power { font-size: 11.5px; font-weight: 600; color: var(--c-follows); background: var(--c-follows-bg); border-radius: 10px; padding: 0 7px; flex: none; }
.colh { font-size: 15px; margin: 0 0 4px; }
.cgroup { margin-top: 12px; }
.cnote { font-size: 12.5px; color: var(--muted); margin: 0 0 6px; line-height: 1.4; }
.coll { display: flex; flex-wrap: wrap; align-items: baseline; gap: 4px 8px; width: 100%; text-align: left; border: 1px solid var(--line); background: var(--bg); border-radius: 8px; padding: 7px 9px; margin-bottom: 6px; color: var(--ink); }
.coll:hover { border-color: var(--accent); }
.coll.on { border-color: var(--accent); background: var(--accent-soft); }
.clogic { font-size: 11.5px; font-weight: 700; color: #fff; background: var(--accent); border-radius: 4px; padding: 0 6px; }
.cprins { font-weight: 600; font-size: 13.5px; }
.ctarget { color: var(--c-follows); }
.cscore { font-size: 12px; color: var(--c-follows); margin-left: auto; }
.cdesc { flex-basis: 100%; font-size: 12.5px; color: var(--muted); line-height: 1.35; }
@media (max-width: 1250px) {
  .layout { grid-template-columns: 284px minmax(0, 1fr); }
  .side.right { grid-column: 1 / -1; position: static; max-height: none; }
  #collections { display: grid; grid-template-columns: repeat(auto-fill, minmax(260px, 1fr)); gap: 0 16px; }
  #collections .colh { grid-column: 1 / -1; }
}

/* ---------- side: checklist ---------- */
.side { background: var(--panel); border: 1px solid var(--line); border-radius: 10px; padding: 12px; position: sticky; top: 12px; max-height: calc(100vh - 24px); overflow: auto; }
.logic { display: flex; flex-wrap: wrap; align-items: center; gap: 6px; padding-bottom: 10px; border-bottom: 1px solid var(--line); margin-bottom: 6px; }
.logic span { font-size: 13px; color: var(--muted); flex-basis: 100%; }
.logic .lbtns { flex-basis: 100%; display: grid; grid-template-columns: repeat(3, 1fr); gap: 6px; }
.sformula { margin: 4px 0 8px; }
.plink { background: none; border: none; padding: 0; font: inherit; color: var(--link); cursor: pointer; text-decoration: underline; }
.linkbtn.inl { margin: 0; font-size: inherit; }
.sformula .stag { font-weight: 600; font-size: 0.9em; color: var(--muted); margin-top: 6px; }
.logic button { border: 1px solid var(--line); background: var(--bg); border-radius: 6px; padding: 3px 12px; font-weight: 600; }
.logic button[aria-pressed="true"] { background: var(--accent); border-color: var(--accent); color: #fff; }
.group { margin-top: 10px; }
.gname { font-size: 11.5px; text-transform: uppercase; letter-spacing: 0.06em; color: var(--muted); margin-bottom: 3px; }
.item { display: flex; align-items: center; gap: 8px; padding: 2px 4px; border-radius: 6px; }
.item.focus { background: var(--accent-soft); }
.tri { display: inline-flex; border: 1px solid var(--line); border-radius: 6px; overflow: hidden; flex: none; }
.tri button { width: 26px; height: 24px; border: 0; background: var(--panel); color: var(--muted); font-size: 13px; padding: 0; }
.tri button + button { border-left: 1px solid var(--line); }
.item.on-yes .t-yes { background: var(--c-follows); color: #fff; }
.item.on-no .t-no { background: var(--c-refuted); color: #fff; }
.item.locked.fixed .t-yes, .item.locked.fixed .t-no { cursor: not-allowed; }
/* settled by the base logic alone: shown checked (or negated), in the same colors as an assumption */
.item.implied.fixed .t-yes, .item.implied.fixed .t-no { cursor: not-allowed; }
.pname { background: none; border: 0; padding: 2px 0; text-align: left; flex: 1; min-width: 0; }
.pname:hover { color: var(--link); }
.reset { margin-top: 14px; width: 100%; border: 1px solid var(--line); background: var(--bg); border-radius: 6px; padding: 6px; }

/* ---------- graph ---------- */
.center { min-width: 0; }
.legend { display: grid; grid-template-columns: repeat(3, max-content); gap: 6px 26px; font-size: 13px; color: var(--muted); margin: 8px 0; }
@media (max-width: 520px) { .legend { grid-template-columns: repeat(2, max-content); } }
.lg { display: inline-flex; align-items: center; gap: 6px; }
.lg b { color: var(--ink); font-weight: 600; }
/* each status's label in its own colour */
.lg.k-follows { color: var(--c-follows); } .lg.k-indep { color: var(--c-indep); } .lg.k-cons { color: var(--c-cons); }
.lg.k-notder { color: var(--c-notder); } .lg.k-open { color: var(--c-open); } .lg.k-refuted { color: var(--c-refuted); }
.lg { font-weight: 600; }
.lg line { stroke-width: 2.5; }
.lg.k-follows line { stroke: var(--c-follows); }
.lg.k-indep line { stroke: var(--c-indep); stroke-dasharray: 5 4; }
.lg.k-cons line { stroke: var(--c-cons); stroke-width: 3; stroke-dasharray: 0 5.5; stroke-linecap: round; }
.lg.k-notder line { stroke: var(--c-notder); stroke-opacity: 0; }
.lg.k-notder svg { border: 1.5px solid var(--c-notder); border-radius: 5px; height: 12px; width: 22px; }
.lg.k-open svg { border: 1.5px dashed var(--c-open); border-radius: 5px; height: 12px; width: 22px; }
.lg.k-open line { stroke-opacity: 0; }
.lg.k-refuted line { stroke: var(--c-refuted); }

.graphbox { background: var(--panel); border: 1px solid var(--line); border-radius: 10px; }
#graph { display: block; width: 100%; height: auto; }
.edge { fill: none; stroke-width: 1.8; opacity: .85; }
.edge.k-follows { stroke: var(--c-follows); }
.edge.k-indep { stroke: var(--c-indep); stroke-dasharray: 6 5; }
.edge.k-cons { stroke: var(--c-cons); stroke-dasharray: 0 6; stroke-linecap: round; stroke-width: 2.8; }
.edge.k-refuted { stroke: var(--c-refuted); stroke-width: 2; }
.edge.hover, .edge.focus { stroke-width: 3.2; opacity: 1; }
.hubrect { fill: var(--c-follows-bg); stroke: var(--c-follows); stroke-width: 1.5; }
.hub { cursor: pointer; }
.hub:focus-visible { outline: none; }
.hub:focus-visible .hubrect, .hubrect.focus { stroke-width: 3; }
.hubrect.bad { fill: var(--c-refuted-bg); stroke: var(--c-refuted); }
.hub text { font: 500 14px var(--sans); fill: var(--ink); }
.hub text.hubtitle { font-weight: 700; }
.node { cursor: pointer; }
.node rect { stroke-width: 1.5; fill: var(--panel); stroke: var(--line); }
.node text { font: 500 13px var(--sans); fill: var(--ink); pointer-events: none; }
.node.k-follows rect { fill: var(--c-follows-bg); stroke: var(--c-follows); }
.node.k-indep rect { fill: var(--c-indep-bg); stroke: var(--c-indep); }
.node.k-cons rect { fill: var(--c-cons-bg); stroke: var(--c-cons); }
.node.k-notder rect { fill: var(--c-notder-bg); stroke: var(--c-notder); }
.node.k-open rect { fill: var(--c-open-bg); stroke: var(--c-open); stroke-dasharray: 4 3; }
.node.k-refuted rect { fill: var(--c-refuted-bg); stroke: var(--c-refuted); }
.node.k-refuted text { text-decoration: line-through; text-decoration-thickness: 1px; }
.node.hover rect, .node.focus rect { stroke-width: 3; }

#banner .bad { background: var(--c-refuted-bg); border: 1px solid var(--c-refuted); border-radius: 8px; padding: 10px 14px; margin-bottom: 8px; }

/* ---------- details ---------- */
.details { background: var(--panel); border: 1px solid var(--line); border-radius: 10px; padding: 14px 18px; margin-top: 14px; scroll-margin-top: 12px; }
.details .hint { color: var(--muted); }
.dhead { display: flex; align-items: baseline; gap: 12px; flex-wrap: wrap; }
.dhead h3 { font: 600 22px var(--serif); margin: 0; }
.dgroup { color: var(--muted); font-size: 13px; }
.formula { overflow-x: auto; overflow-y: hidden; padding: 2px 0; }
.gloss { margin: 4px 0 10px; font-family: var(--serif); font-size: 16px; }
.st { margin: 8px 0; }
.pill { display: inline-block; border-radius: 999px; padding: 1px 10px; font-weight: 600; font-size: 13px; border: 1.5px solid; margin-right: 4px; }
.pill.k-follows { color: var(--c-follows); background: var(--c-follows-bg); }
.pill.k-indep { color: var(--c-indep); background: var(--c-indep-bg); }
.pill.k-cons { color: var(--c-cons); background: var(--c-cons-bg); }
.pill.k-notder { color: var(--c-notder); background: var(--c-notder-bg); }
.pill.k-open { color: var(--c-open); background: var(--c-open-bg); }
.pill.k-refuted { color: var(--c-refuted); background: var(--c-refuted-bg); }
.details h4 { margin: 14px 0 4px; font-size: 13px; text-transform: uppercase; letter-spacing: 0.05em; color: var(--muted); }
.steps { margin: 4px 0; padding-left: 22px; }
.steps li { margin: 3px 0; }
.steps .by { color: var(--muted); }
.steps .contra { color: var(--c-refuted); }
.stepnote { color: var(--muted); font-size: 13.5px; }
.src { display: inline-block; font-size: 12px; border: 1px solid var(--line); border-radius: 4px; padding: 0 5px; color: var(--accent); white-space: nowrap; vertical-align: 1px; }
.src.added { color: var(--c-notder); border-color: var(--c-notder); }
.model { border-left: 3px solid var(--accent); padding: 4px 0 4px 12px; margin: 4px 0 8px; }
.mname { font-weight: 600; }
.mdesc { color: var(--muted); font-size: 14px; }
.mline { margin-top: 4px; }
.subtle { color: var(--muted); font-size: 13.5px; }
.openq { color: var(--muted); font-style: italic; }
.dactions { display: flex; flex-wrap: wrap; gap: 8px; margin-top: 14px; }
.dactions button { border: 1px solid var(--line); background: var(--bg); border-radius: 6px; padding: 5px 12px; }
.dactions button[aria-pressed="true"] { border-color: var(--accent); background: var(--accent-soft); }
.dactions button:disabled { opacity: .5; cursor: not-allowed; }

/* ---------- strength (Hasse diagram) ---------- */
.shead { background: var(--panel); border: 1px solid var(--line); border-radius: 10px; padding: 4px 18px; margin-bottom: 14px; }
.skey { display: flex; flex-wrap: wrap; gap: 6px 22px; color: var(--muted); font-size: 13.5px; }
.skey span { display: inline-flex; align-items: center; gap: 8px; }
.sbox { background: var(--panel); border: 1px solid var(--line); border-radius: 10px; overflow-x: auto; }
.sbox svg { display: block; height: auto; margin: 0 auto; }
.se { stroke-width: 2; }
.se.strict { stroke: var(--ink); opacity: .75; }
.se.unk { stroke: var(--c-notder); stroke-dasharray: 6 5; }
.sq { font: 700 14px var(--sans); fill: var(--c-notder); }
.sn { cursor: pointer; }
.sn rect { fill: var(--panel); stroke: var(--accent); stroke-width: 1.5; }
.sn text { font: 500 13px var(--sans); fill: var(--ink); pointer-events: none; }
.sn.basenode rect { fill: var(--c-follows-bg); stroke: var(--c-follows); }
.sn.focus rect, .sn:hover rect { stroke-width: 3; }
.strength .bad { background: var(--c-refuted-bg); border: 1px solid var(--c-refuted); border-radius: 8px; padding: 10px 14px; }

/* ---------- catalogue / about ---------- */
.catalogue section, .about section { background: var(--panel); border: 1px solid var(--line); border-radius: 10px; padding: 6px 20px 14px; margin-bottom: 16px; }
.catalogue h2, .about h2 { font: 600 20px var(--serif); margin: 14px 0 8px; }
.about h3 { font: 600 16px var(--serif); margin: 16px 0 4px; }
.about { max-width: 80ch; }
.ctable { border-collapse: collapse; width: 100%; }
.ctable td { border-top: 1px solid var(--line); padding: 8px 10px 8px 0; vertical-align: top; }
.ctable td:last-child { overflow-x: auto; max-width: 0; width: 100%; }
.ctag { font-weight: 600; white-space: nowrap; }
.cg { color: var(--muted); font-size: 14px; margin-top: 2px; }
.clist { padding-left: 20px; }
.clist li { margin: 6px 0; }
.cn { color: var(--muted); font-size: 14px; }
.mcard { border-top: 1px solid var(--line); padding: 10px 0; }
.mvals { margin-top: 6px; display: flex; flex-wrap: wrap; gap: 4px; }
.mv { font-size: 12.5px; border-radius: 4px; padding: 1px 6px; border: 1px solid; }
.mv.t { color: var(--c-follows); background: var(--c-follows-bg); }
.mv.f { color: var(--c-refuted); background: var(--c-refuted-bg); }
.mv.derived { opacity: .6; border-style: dashed; }
footer { color: var(--muted); font-size: 13px; padding-bottom: 30px; }

.leanb { display: inline-block; font-size: 11.5px; font-weight: 600; border-radius: 4px; padding: 0 6px; color: #fff; background: var(--c-follows); text-decoration: none; white-space: nowrap; vertical-align: 1px; }
.leanb:hover { filter: brightness(1.1); }
a.mv { text-decoration: none; }

/* the rotated type quantifiers */
.tq { display: inline-block; transform: rotate(180deg); }

@media (max-width: 900px) {
  .layout { grid-template-columns: 1fr; }
  .side { position: static; max-height: none; }
  #checklist { display: grid; grid-template-columns: repeat(auto-fill, minmax(150px, 1fr)); gap: 0 10px; }
  .group { grid-column: 1 / -1; display: contents; }
  .gname { grid-column: 1 / -1; margin-top: 10px; }
  header h1 { font-size: 28px; }
}

/* ---------- "show only ◆" filter ---------- */
.onlynew { display: flex; gap: 8px; align-items: center; background: var(--panel); border: 1px solid var(--line); border-radius: 10px; padding: 10px 16px; margin-bottom: 16px; cursor: pointer; }
.only-new .nonew, .only-new .clist li:not(.isnew), .only-new .mcard:not(.isnew), .only-new .mcard .mv:not(.isnew) { display: none; }

/* base-logic window */
.logic .showlogic { flex-basis: 100%; margin-top: 6px; background: none; border: none; padding: 0; color: var(--link); text-decoration: underline; cursor: pointer; font: inherit; font-size: 0.85em; text-align: left; font-weight: normal; }
.logicdlg { width: min(860px, calc(100vw - 32px)); max-height: calc(100vh - 48px); padding: 0; border: 1px solid var(--line); border-radius: 10px; background: var(--panel); color: var(--ink); }
.logicdlg::backdrop { background: rgba(0, 0, 0, 0.35); }
.logicdlg .lhead { position: sticky; top: 0; z-index: 1; display: flex; flex-wrap: wrap; align-items: center; gap: 12px; padding: 14px 18px; background: var(--panel); border-bottom: 1px solid var(--line); }
.logicdlg .lhead h2 { margin: 0; font-size: 1.1em; }
.logicdlg .lclose { margin-left: auto; font: inherit; background: none; border: none; color: var(--muted); cursor: pointer; font-size: 1.1em; }
.logicbody { padding: 4px 18px 18px; overflow-x: auto; }
.lsec h4 { margin: 18px 0 6px; }
.lsec.ladded { border-left: 3px solid var(--accent); padding-left: 10px; }
.lbadge { font-size: 0.75em; font-weight: normal; color: var(--accent); background: var(--accent-soft); border-radius: 4px; padding: 1px 6px; margin-left: 6px; }
.lblurb { margin-top: 12px; }
.llang summary { cursor: pointer; color: var(--muted); }
.lsec .katex-display { margin: 4px 0; text-align: left; font-weight: normal; }
.lsec .katex-display > .katex { text-align: left; font-weight: normal; }

.detailstack { scroll-margin-top: 12px; }
.details.current { border-color: var(--accent); }
.dclose { margin-left: auto; background: none; border: none; color: var(--muted); font-size: 16px; cursor: pointer; padding: 0 2px; }
.logiccard .dhead { margin-top: 4px; }
.logiccard .hint { margin-bottom: 12px; }
.linkbtn { margin-left: auto; background: none; border: none; padding: 0; color: var(--link); text-decoration: underline; cursor: pointer; font: inherit; font-size: 13px; }
.logiccard .lblurb { color: var(--muted); }
.logiccard .katex-display { overflow-x: auto; overflow-y: hidden; padding-bottom: 2px; }

/* the six status checkboxes, two to a row, each in its status's colour */
.logic .statusfilters { flex-basis: 100%; display: grid; grid-template-columns: 1fr 1fr; gap: 5px 8px; margin-top: 10px; font-size: 0.85em; }
.statusfilters .sf { display: flex; align-items: center; gap: 6px; font-weight: 600; cursor: pointer; white-space: nowrap; }
.statusfilters .sf input { width: 15px; height: 15px; margin: 0; cursor: pointer; }
.sf.k-follows { color: var(--c-follows); } .sf.k-follows input { accent-color: var(--c-follows); }
.sf.k-indep { color: var(--c-indep); } .sf.k-indep input { accent-color: var(--c-indep); }
.sf.k-cons { color: var(--c-cons); } .sf.k-cons input { accent-color: var(--c-cons); }
.sf.k-notder { color: var(--c-notder); } .sf.k-notder input { accent-color: var(--c-notder); }
.sf.k-open { color: var(--c-open); } .sf.k-open input { accent-color: var(--c-open); }
.sf.k-refuted { color: var(--c-refuted); } .sf.k-refuted input { accent-color: var(--c-refuted); }
.sf.sf-thm { grid-column: 1 / -1; color: var(--muted); } .sf.sf-thm input { accent-color: var(--accent); }
.logicdlg .ltabs { display: flex; gap: 4px; }
.logicdlg .ltabs button { font: inherit; padding: 4px 12px; border: 1px solid var(--line); border-radius: 6px; background: var(--bg); color: var(--ink); cursor: pointer; }
.logicdlg .ltabs button[aria-selected="true"] { background: var(--accent); border-color: var(--accent); color: var(--panel); }
.sm.strict { fill: var(--ink); opacity: .75; }
.sm.unk { fill: var(--c-notder); }

/* how many principles to show */
.levelsel { display: flex; flex-wrap: wrap; align-items: center; gap: 6px; margin: 6px 0 2px; font-size: 0.85em; color: var(--muted); }
.levelsel .lvbtns { display: flex; gap: 4px; }
.levelsel button { border: 1px solid var(--line); background: var(--bg); color: var(--ink); border-radius: 6px; padding: 1px 5px; font-size: 0.9em; white-space: nowrap; }
.levelsel button[aria-pressed="true"] { background: var(--accent); border-color: var(--accent); color: #fff; }
.highlights .hl h3 { margin-top: 12px; }
.highlights .hlsee { color: var(--muted); font-size: 14px; }
.highlights .hllean, .catalogue .hllean { font-size: 13px; color: var(--muted); }
.highlights .hllean .leanb, .catalogue .hllean .leanb { font-family: ui-monospace, SFMono-Regular, Menlo, monospace; }
.catalogue .hllean { display: block; margin-top: 3px; }
/* the language description stays one line, so that switching languages does not move the page */
@media (min-width: 700px) { .langnote { max-width: none; white-space: nowrap; overflow: hidden; text-overflow: ellipsis; } }
/* ---------- the Simply Typed Lambda Calculus view ---------- */
.kclass { display: inline-flex; flex-wrap: wrap; align-items: center; gap: 6px; margin-left: 14px; padding-left: 14px; border-left: 1px solid var(--line); }
.sttm { font-size: 12px; font-weight: 600; margin-left: 4px; color: var(--muted); cursor: help; }
.item.stt-inst .sttm { color: #a15c00; }
.item.stt-lost .sttm { color: var(--c-refuted); }
.item.stt-lost .pname { text-decoration: line-through; color: var(--muted); }
.item.stt-lost { opacity: 0.75; }
.item .tri button:disabled { opacity: 0.35; cursor: not-allowed; }
.node.k-lost rect { fill: var(--bg); stroke: var(--c-open); stroke-dasharray: 4 3; }
.node.k-lost text { fill: var(--muted); text-decoration: line-through; text-decoration-thickness: 1px; }
.shelflabel { font: 600 12.5px var(--sans); fill: var(--muted); }
.sttbanner { font-size: 13px; line-height: 1.45; color: var(--ink); background: var(--panel); border: 1px solid var(--line); border-radius: 8px; padding: 8px 12px; margin: 6px 0; }
.sttbanner .aside { color: var(--muted); }
.coll.lost { opacity: 0.5; cursor: not-allowed; }
.coll.lost .cprins { text-decoration: line-through; }
@media (prefers-color-scheme: dark) { :root:not([data-theme="light"]) .item.stt-inst .sttm { color: #e0a24a; } }
:root[data-theme="dark"] .item.stt-inst .sttm { color: #e0a24a; }
.item.stt-open .sttm { color: var(--c-open); }
.item.stt-open .pname { color: var(--muted); font-style: italic; }