:root{--ink: #1a1a1a;--ink-soft: #5c5853;--ink-faint: #6b655d;--ink-ghost: #9a938c;--paper: #fdfcfa;--parchment: #f7f5f0;--parchment-deep: #f1eee7;--rule: #e0dad0;--rule-soft: #e8e2d8;--accent: #8c1515;--accent-deep: #820000;--accent-bright: #b1040e;--accent-muted: #c58a8a;--accent-wash: #f6e9e8;--verified: #2f6b46;--verified-wash: #e4efe6;--axiom: #b45309;--axiom-wash: #fbe3c4;--sorry: #a33333;--sorry-wash: #f6d6d6;--warning: #c99806;--lean: #35507a;--lean-wash: #edf1f6;--lean-line: #a9b9ce;--fs-2xs: .72rem;--fs-xs: .78rem;--fs-sm: .85rem;--fs-body-s: .95rem;--fs-body: 1rem;--fs-md: 1.15rem;--fs-lg: 1.35rem;--fs-xl: 2rem;--fs-hero: 2.4rem;--sp-1: .25rem;--sp-2: .5rem;--sp-3: .75rem;--sp-4: 1rem;--sp-6: 1.5rem;--sp-8: 2rem;--sp-12: 3rem;--sp-16: 4rem;--r-badge: 3px;--r-card: 6px;--r-frame: 8px;--r-pill: 999px}:where(a,button,summary,input,[tabindex]):focus-visible{outline:2px solid var(--lean);outline-offset:2px;border-radius:2px}@media(prefers-reduced-motion:reduce){*,*:before,*:after{transition-duration:.001ms!important;animation-duration:.001ms!important}}@font-face{font-family:JuliaMono;src:url(https://cdn.jsdelivr.net/gh/cormullion/juliamono@master/webfonts/JuliaMono-Regular.woff2) format("woff2");font-weight:400;font-style:normal;font-display:swap}@font-face{font-family:JuliaMono;src:url(https://cdn.jsdelivr.net/gh/cormullion/juliamono@master/webfonts/JuliaMono-Bold.woff2) format("woff2");font-weight:700;font-style:normal;font-display:swap}:root{--code-font: "JuliaMono", ui-monospace, "SF Mono", Menlo, Consolas, monospace}article.library{max-width:860px;margin:0 auto;padding:3rem 1.5rem 6rem;font-family:Charter,Georgia,Times New Roman,serif;line-height:1.6}article.library h1{font-weight:400;font-size:1.9rem}article.library a{color:#820000;text-decoration:none;border-bottom:1px dotted #C58A8A}article.library a:hover{border-bottom-style:solid}.site-nav{position:sticky;top:0;z-index:20;font-size:var(--fs-sm);color:var(--accent);margin:0 0 1.4rem;padding:.6rem 0;background:var(--paper);border-bottom:1px solid var(--rule);display:flex;align-items:baseline;gap:.25rem .9rem;flex-wrap:wrap}.site-nav .site-nav-kicker{flex:0 0 100%;letter-spacing:.16em;text-transform:uppercase;font-size:.68rem;padding-right:9rem}.site-nav .site-nav-commit{position:absolute;top:.6rem;right:0;white-space:nowrap}.site-nav a{border-bottom:1px dotted #C58A8A}.site-nav .site-nav-current{color:#2e2d29;font-weight:600}.lib-search{position:relative;margin:1.4rem 0 .6rem}.lib-search input{width:100%;font-family:var(--code-font);font-size:.85rem;padding:.55rem .8rem;border:1px solid #D8D0C5;border-radius:6px;background:#fdfcfa;color:#36342f}.lib-search input:focus{outline:2px solid var(--lean);border-color:var(--lean)}#lib-search-results{position:absolute;z-index:30;left:0;right:0;top:100%;max-height:24rem;overflow-y:auto;background:#fdfcfa;border:1px solid #D8D0C5;border-top:none;border-radius:0 0 6px 6px;box-shadow:0 10px 24px #50411e26}#lib-search-results .hit{display:grid;grid-template-columns:4.6rem 1fr;grid-template-rows:auto auto;column-gap:.6rem;padding:.45rem .7rem;border-bottom:1px solid #EFEBE3;border-radius:0}#lib-search-results .hit:hover{background:#f7f5f0}#lib-search-results .hit-kind{grid-row:1 / 3;font-size:.68rem;color:#a0151d;text-transform:uppercase;align-self:start;padding-top:.15rem}#lib-search-results .hit-name{font-family:var(--code-font);font-size:.82rem;font-weight:600}#lib-search-results .hit-mod{font-size:.7rem;color:#8c1515;margin-left:.5rem}#lib-search-results .hit-nl{grid-column:2;font-size:.78rem;color:#544f4a}#lib-search-results .no-hit{padding:.6rem .8rem;color:#8c1515;font-style:italic}.lib-footnote{font-size:.78rem;color:#8c1515}.module-block{border-top:1px solid #E0DAD0;padding:.4rem 0;margin:0}.module-block>summary{cursor:pointer;list-style-position:outside;padding:.55rem .2rem}.module-block>summary:hover{background:#fdfcfa}.module-block .module-name{font-size:1.15rem;color:#2e2d29}.module-block .module-counts{font-size:.72rem;color:#a0151d;margin-left:.7rem;white-space:nowrap}.module-block .module-brief{display:block;font-size:.88rem;color:#544f4a;margin:.15rem 0 0 1.05rem}.module-block .module-headlines{display:flex;flex-wrap:wrap;gap:.35rem;margin:.35rem 0 0 1.05rem}.module-block .hl-chip{font-family:var(--code-font);font-size:var(--fs-2xs);color:var(--accent);background:var(--accent-wash);padding:.05rem .4rem;border-radius:var(--r-badge);white-space:nowrap}.module-block .hl-extra{display:none}.module-block .module-headlines.show-all .hl-extra{display:inline-block}.module-block .hl-more{font:inherit;font-size:var(--fs-2xs);color:var(--ink-faint);background:none;border:none;padding:0;cursor:pointer;align-self:center;border-bottom:1px dotted var(--accent-muted)}.module-block .hl-more:hover{color:var(--accent)}.lib-tools{display:flex;align-items:center;gap:.4rem;margin:.6rem 0 .4rem}.lib-tools button{font:inherit;font-size:var(--fs-2xs);color:var(--ink-soft);background:var(--paper);border:1px solid var(--rule);border-radius:var(--r-pill);padding:.15rem .7rem;cursor:pointer}.lib-tools button:hover{background:var(--parchment-deep);color:var(--ink)}.back-to-top{position:fixed;left:1.4rem;bottom:1.4rem;z-index:50;display:inline-flex;align-items:center;gap:.35rem;font:inherit;font-size:var(--fs-2xs);color:var(--ink-soft);background:var(--paper);border:1px solid var(--rule);border-radius:var(--r-pill);padding:.35rem .8rem;cursor:pointer;box-shadow:0 2px 8px #0000001f;opacity:0;visibility:hidden;transform:translateY(.5rem);transition:opacity .18s ease,transform .18s ease,visibility .18s}.back-to-top.visible{opacity:1;visibility:visible;transform:translateY(0)}.back-to-top:hover{background:var(--parchment-deep);color:var(--ink)}@media(prefers-reduced-motion:reduce){.back-to-top{transition:opacity .18s ease,visibility .18s;transform:none}.back-to-top.visible{transform:none}}.module-block .module-doc{font-size:.92rem;color:#43403b;margin:.4rem 0 .6rem;padding-left:1.05rem}.module-block .module-doc h1{display:none}.module-block:not(.depth-0){border-top:none;border-left:2px solid #E8E2D8;margin-left:.55rem;padding-left:.7rem}.module-block.depth-1 .module-name{font-size:1.02rem}.module-block.depth-2 .module-name,.module-block.depth-3 .module-name{font-size:.95rem}.module-block:not(.depth-0)>summary{padding:.4rem .2rem}article.library h2{font-weight:400;font-size:1.35rem;margin-top:2.4rem;border-bottom:1px solid #E0DAD0;padding-bottom:.3rem}article.library .lib-byline{color:#8c1515;font-size:.85rem;margin-bottom:2rem}article.library .lib-byline a{color:inherit}article.library .lib-intro{font-size:.95rem}.lib-hero-stats{display:flex;flex-wrap:wrap;gap:0;margin:.6rem 0 1.2rem}.lib-hero-stats>div{padding:0 var(--sp-6);border-left:1px solid var(--rule)}.lib-hero-stats>div:first-child{padding-left:0;border-left:none}.lib-hero-stats dt{font-size:var(--fs-2xs);letter-spacing:.07em;text-transform:uppercase;color:var(--ink-faint);margin:0 0 .15rem}.lib-hero-stats dd{margin:0;font-size:1.6rem;line-height:1.1;color:var(--accent);font-variant-numeric:tabular-nums}.lib-hero-stats dd .unit{font-size:1rem;margin-left:.05rem}.lib-hero-stats dd.clean{color:var(--verified)}.lib-hero-stats dd.warn{color:var(--sorry)}.area-table{width:100%;border-collapse:collapse;font-size:var(--fs-body-s);margin-top:1.4rem}.area-table th,.area-table td{text-align:left;padding:.55rem .6rem;border-bottom:1px solid var(--rule-soft);vertical-align:middle}.area-table th{font-weight:600;color:var(--ink-faint);font-size:var(--fs-2xs);text-transform:uppercase;letter-spacing:.04em}.area-table tbody tr{--cell-bg: var(--paper)}.area-table tbody tr:hover{background:var(--parchment);--cell-bg: var(--parchment)}.area-table th:first-child,.area-table td:first-child{white-space:nowrap;width:1%}.area-table td:first-child a{font-weight:600}.area-table td.num{text-align:right;font-variant-numeric:tabular-nums}.area-table td.intro-cell{color:var(--ink-soft);position:relative}.area-table .intro-clamp{display:-webkit-box;-webkit-line-clamp:4;line-clamp:4;-webkit-box-orient:vertical;overflow:hidden}.area-table .intro-clamp.expanded{display:block;-webkit-line-clamp:unset;line-clamp:unset;overflow:visible}.area-table .intro-toggle{position:absolute;right:.6rem;bottom:.55rem;font:inherit;font-size:var(--fs-2xs);color:var(--accent-deep);border:none;cursor:pointer;padding:0 0 0 2rem;background:linear-gradient(to right,transparent,var(--cell-bg) 1.6rem)}.area-table .intro-toggle:hover{text-decoration:underline}.size-cell,.review-cell{width:7.5rem}.area-table .stat-n{display:block}.area-table .stat-of{color:var(--ink-ghost)}.bar{display:block;height:5px;margin-top:.28rem;background:var(--parchment-deep);border-radius:var(--r-badge);overflow:hidden}.bar-fill{display:block;height:100%;border-radius:var(--r-badge)}.bar-review{background:var(--verified)}.glyph-clean{color:var(--ink-ghost)}.badge-sorried{background:var(--sorry-wash);color:var(--sorry);font-size:var(--fs-2xs);padding:.08rem .45rem;border-radius:var(--r-badge);font-variant-numeric:tabular-nums}.decl-card{border:1px solid var(--rule-soft);border-left:3px solid var(--accent-bright);border-radius:var(--r-card);background:var(--paper);padding:.7rem 1rem .6rem;margin:1.1rem 0}.decl-card.kind-theorem{border-left-color:#8c1515}.decl-card.kind-structure,.decl-card.kind-class,.decl-card.kind-inductive{border-left-color:#888;background:#f6f6f4}.decl-card.kind-axiom{border-left-color:#b45309;background:#f7f5f0}.decl-head{display:flex;align-items:baseline;gap:.55rem;flex-wrap:wrap}.decl-name{font-family:var(--code-font);font-size:.95rem;font-weight:600;min-width:0;overflow-wrap:anywhere}.decl-ns{font-family:var(--code-font);font-size:.8rem;font-weight:400;color:var(--ink-ghost);margin-top:.1rem}.decl-kind{font-size:.72rem;color:#fff;background:#a0151d;border-radius:3px;padding:.08rem .4rem;text-transform:uppercase;letter-spacing:.04em}.badge{font-size:.72rem;border-radius:3px;padding:.08rem .45rem}.badge-reviewed{background:#dcefdc;color:#2e6b2e}.badge-stale{background:#f6e9e8;color:#8c1515}.badge-unreviewed{background:#eee;color:#777}.badge-sorry{background:#f6d6d6;color:#a33}.badge-axiom{background:#f6e9e8;color:#a0151d}.badge-flagged{background:#fbe3c4;color:#8a5300}.flag-notes{margin:.3rem 0 .4rem;padding-left:1.2rem;list-style:none}.flag-notes li{font-size:.85rem;color:#8a5300;display:flex;gap:.5rem;align-items:flex-start}.flag-note-text{flex:1;min-width:0}.flag-remove{display:none;flex:none;margin-top:.1rem;font-size:.7rem;line-height:1;background:none;border:none;color:#b89a6a;cursor:pointer;padding:0;opacity:.6}.flag-remove:hover{color:#8c1515;opacity:1}body.review-mode .flag-remove{display:inline}.flag-remove:hover{background:#8c1515;color:#fff;border-color:#8c1515}.badge-paper{background:#f6e9e8;color:#8c1515;text-decoration:none}.badge-paper:hover{background:#c58a8a;color:#fff}.review-tag{display:none;font-size:.7rem;border-radius:3px;padding:.05rem .4rem;margin-left:.5rem;background:#fbe3c4;color:#8a5300;font-weight:600;white-space:nowrap;vertical-align:middle}.badge-reviewed,.badge-stale,.badge-unreviewed,.badge-flagged{display:none}body.review-mode .review-tag{display:inline-block}body.review-mode .badge-reviewed,body.review-mode .badge-stale,body.review-mode .badge-unreviewed{display:inline}body.review-mode .badge-flagged:not([hidden]){display:inline}.flag-notes{display:none}body.review-mode .flag-notes{display:block}#review-mode-toggle{position:fixed;right:.9rem;bottom:.9rem;z-index:50;font-size:.78rem;padding:.3rem .7rem;border-radius:4px;border:1px solid #D8CFBE;background:#fbf8f1;color:#4d4f53;cursor:pointer;box-shadow:0 1px 4px #0000001f}#review-mode-toggle:hover{background:#f1eee7;color:#2e2d29}.decl-nl{margin:.45rem 0 .2rem;font-size:var(--fs-body);color:var(--ink)}.decl-nl p{margin:.3rem 0}.decl-nl.nl-missing{color:#999;font-style:italic}.decl-card details{margin-top:.35rem}.decl-card summary{cursor:pointer;font-size:.8rem;color:#4d4f53}.decl-stmt{position:relative;font-family:var(--code-font);font-size:.8rem;line-height:1.55;background:#f1eee7;border-radius:4px;padding:.6rem .8rem;margin:.4rem 0}.decl-stmt-wrap{white-space:pre-wrap;overflow-wrap:anywhere}.decl-stmt-scrollable{white-space:pre;overflow-x:auto}.decl-stmt-scrollable.has-copy{overflow:visible}.decl-stmt-scroll{overflow-x:auto;white-space:pre}.copy-btn{position:absolute;top:.3rem;right:.3rem;font-family:inherit;font-size:.68rem;line-height:1;padding:.2rem .45rem;border:1px solid #D8CFBE;border-radius:3px;background:#fbf8f1;color:#6b655d;cursor:pointer;opacity:0;transition:opacity .12s ease,background .12s ease,color .12s ease}.decl-stmt:hover .copy-btn,.copy-btn:focus-visible{opacity:1}.copy-btn:hover{background:#f1eee7;color:#2e2d29}.copy-btn.copied{opacity:1;background:#dcefdc;color:#2e6b2e;border-color:#bcdcbc}@media(hover:none){.copy-btn{opacity:.55}}.decl-stmt a{color:#8c1515;font-weight:600;border-bottom:none}.decl-stmt a:hover{border-bottom:1px solid #C58A8A}.decl-stmt a.ext-link{color:#5e5953;font-weight:500}.decl-stmt a.ext-link:hover{border-bottom:1px dashed #9A938C}.decl-stmt.stmt-structured{white-space:normal}.stmt-section-label{font-size:var(--fs-2xs);font-weight:700;text-transform:uppercase;letter-spacing:.07em;color:var(--accent);margin-bottom:.15rem}.stmt-rows{display:flex;flex-direction:column}.stmt-row{display:grid;grid-template-columns:max-content 1fr;column-gap:.6rem;align-items:start;padding:.15rem 0 .15rem .6rem;border-left:2px solid var(--rule);border-bottom:1px solid var(--rule-soft);line-height:1.25}.stmt-rows .stmt-row:last-child{border-bottom:none}.stmt-row:hover{background:var(--parchment)}.stmt-row.hyp{border-left-color:var(--lean)}.stmt-comment{font-style:italic;font-size:.78rem;color:var(--ink-faint);padding:.3rem 0 .05rem .6rem}.stmt-row-label{display:flex;gap:.3rem;font-weight:600;white-space:nowrap}.stmt-row-colon{font-weight:400;color:var(--ink-faint)}.stmt-body-span{grid-column:1 / -1}.stmt-body{min-width:0}.stmt-line{overflow-x:auto;white-space:pre;padding-bottom:1px}.stmt-line+.stmt-line{margin-top:.02rem}.stmt-line,.decl-stmt-scroll,.decl-stmt-scrollable{scrollbar-width:thin;scrollbar-color:var(--rule) transparent}.stmt-line::-webkit-scrollbar,.decl-stmt-scroll::-webkit-scrollbar,.decl-stmt-scrollable::-webkit-scrollbar{height:6px}.stmt-line::-webkit-scrollbar-track,.decl-stmt-scroll::-webkit-scrollbar-track,.decl-stmt-scrollable::-webkit-scrollbar-track{background:transparent}.stmt-line::-webkit-scrollbar-thumb,.decl-stmt-scroll::-webkit-scrollbar-thumb,.decl-stmt-scrollable::-webkit-scrollbar-thumb{background:var(--rule);border-radius:3px}.stmt-line:hover::-webkit-scrollbar-thumb,.decl-stmt-scroll:hover::-webkit-scrollbar-thumb,.decl-stmt-scrollable:hover::-webkit-scrollbar-thumb{background:var(--ink-ghost)}.stmt-concl{margin-top:.35rem;padding:.3rem 0 .05rem .6rem;border-top:1px solid var(--rule-soft);line-height:1.25}.stmt-concl .stmt-section-label{margin-bottom:.15rem}.stmt-fields.bordered{margin-top:.35rem;padding-top:.3rem;border-top:1px solid var(--rule-soft)}.stmt-fields .stmt-section-label{margin-bottom:.15rem}.chain{margin:.15rem 0 .05rem}.chain-line{display:flex;gap:.5rem;align-items:baseline}.chain-tag{flex:0 0 auto;width:2.1rem;font-family:Charter,Georgia,serif;font-size:.72rem;font-style:italic;color:var(--ink-faint)}.chain-lines{flex:1 1 auto;min-width:0}.chain-rule{border-top:1px solid var(--rule);margin:.15rem 0 .15rem 2.6rem}.decl-nl .nl-link{text-decoration:underline dashed var(--lean-line);text-decoration-thickness:1px;text-underline-offset:3px;border-radius:2px;transition:background .12s ease,text-decoration-color .12s ease}.decl-nl .nl-link.xl-hot{background:var(--lean-wash);text-decoration-color:var(--lean)}.decl-nl .nl-link:focus-visible{outline:2px solid var(--lean);outline-offset:1px}.stmt-row.xl-hot{background:var(--lean-wash);border-left-color:var(--lean)}.stmt-concl-body{border-radius:3px;transition:background .12s ease,box-shadow .12s ease}.stmt-concl-body.xl-hot{background:var(--lean-wash);box-shadow:inset 2px 0 0 var(--lean)}@media(prefers-reduced-motion:reduce){.decl-nl .nl-link,.stmt-row,.stmt-concl-body{transition:none}}.decl-meta{font-size:.75rem;color:#8c1515;margin-top:.3rem}.decl-meta a{color:inherit}.decl-meta code{font-size:.72rem}.helper-block>summary{cursor:pointer;font-size:.85rem;color:#4d4f53;margin-top:.8rem}.helper-list{font-size:.85rem;list-style:none;padding-left:.4rem}.helper-list li{margin:.25rem 0}.helper-list code{font-size:.82rem}.helper-item>summary{cursor:pointer}.helper-item>summary:hover code{color:#820000}.helper-item .helper-kind{font-size:.68rem;color:#a0151d;text-transform:uppercase;margin-left:.45rem}.helper-item .helper-nl{color:#544f4a}.helper-item .decl-stmt{font-size:.76rem;margin:.35rem 0 .2rem}.helper-item .decl-meta{margin-bottom:.45rem}.decl-card.flash-target{outline:2px solid #B1040E;background:#f6e9e8}.review-controls{display:none;margin-left:auto;gap:.4rem}body.review-mode .review-controls{display:inline-flex}.review-controls button{font-family:Charter,Georgia,serif;font-size:.72rem;color:#4d4f53;background:#fdfcfa;border:1px solid #D8D0C5;border-radius:4px;padding:.1rem .5rem;cursor:pointer}.review-controls button:hover{background:#f1eee7;color:#2e2d29}.graph-placeholder{margin:.6rem 0;padding:2.4rem 1rem;text-align:center;color:var(--ink-faint);font-size:.9rem;border:1px dashed var(--rule);border-radius:var(--r-frame)}.graph-toolbar{display:flex;flex-wrap:wrap;align-items:center;gap:.5rem 1rem;margin:.6rem 0 .4rem;font-size:.85rem;color:#4d4f53}.graph-toolbar button{font:inherit;color:#820000;background:#fdfcfa;border:1px solid #D8D0C5;border-radius:5px;padding:.2rem .7rem;cursor:pointer;white-space:nowrap;flex:none}.graph-toolbar button:hover{background:#f1eee7}#graph-title{flex:1 1 auto;min-width:0}#graph-title{font-weight:600;color:#2e2d29}.graph-legend[hidden]{display:none}.graph-legend{margin-left:auto;display:flex;gap:.8rem;font-size:var(--fs-2xs);text-transform:uppercase;letter-spacing:.04em;color:var(--ink-faint)}.graph-legend .lg-group{display:flex;gap:.8rem}.graph-legend .lg-group+.lg-group{padding-left:.8rem;border-left:1px solid var(--rule)}.graph-legend .lg:before,.graph-legend .lg-ring:before{margin-right:.25rem}.graph-legend .lg:before{content:"●"}.graph-legend .lg-def:before{color:var(--accent-bright)}.graph-legend .lg-structure:before{color:var(--ink-ghost)}.graph-legend .lg-theorem:before{color:var(--lean)}.graph-legend .lg-ring:before{content:"◯";font-weight:700}.graph-legend .lg-sorry:before{color:var(--warning)}#graph-canvas{border:1px solid var(--rule);border-radius:var(--r-frame);background:var(--paper)}.dir-list{margin:.8rem 0}.dir-list.grid{display:grid;grid-template-columns:repeat(auto-fill,minmax(245px,1fr));grid-auto-rows:1fr;gap:.55rem;align-items:stretch}.dir-list.stack{display:flex;flex-direction:column;gap:.45rem}.dir-card{box-sizing:border-box;display:flex;flex-direction:column;gap:.05rem;min-width:0;padding:.45rem .65rem;border:1px solid var(--rule, #DBD4C9);border-radius:6px;text-decoration:none;color:inherit;background:var(--parchment, #FDFCFA)}.dir-list.grid .dir-card{height:100%}.dir-card:hover{background:var(--parchment-deep, #F4F1EA)}.dir-card .module-name{font-weight:600;line-height:1.15;hyphens:manual;overflow-wrap:anywhere}.dir-card .module-counts{font-size:.74rem}.dir-card .module-brief{--dir-brief-lines: 3;margin-top:.1rem;color:var(--ink-soft, #5C5853);font-size:.84rem;line-height:1.35}.dir-list.grid .dir-card .module-brief{display:-webkit-box;-webkit-line-clamp:var(--dir-brief-lines);line-clamp:var(--dir-brief-lines);-webkit-box-orient:vertical;overflow:hidden}.module-doc .doc-h{margin:.6rem 0 .2rem;font-size:.9rem;color:var(--ink-soft, #5C5853);font-variant:small-caps;letter-spacing:.04em}.nav-external span[aria-hidden]{opacity:.55;font-size:.9em}