/* Article geometry and palette follow srush/lean-transformer site/tufte.css
   and site/verso-tufte.css. Lean's generated interaction styles stay intact. */
@font-face{font-family:et-book;src:url('https://srush.github.io/DiffRast/docs/et-book/et-book-roman-line-figures/et-book-roman-line-figures.woff') format('woff');font-display:swap}
:root{color-scheme:light;--verso-text-color:#404444;--verso-background-color:#fff;--verso-code-box-background-color:#f8f8f8;--verso-link-color:#305c78}
*{box-sizing:border-box}html{font-size:15px;scroll-behavior:smooth}body{width:58rem;max-width:100%;margin:0 auto;padding:0 2rem 8rem;background:#fff;color:#404444;font-family:et-book,Palatino,'Palatino Linotype',Georgia,serif}main{width:100%}header{position:relative;padding-top:1rem}h1{font-size:3.2rem;font-weight:400;line-height:1.15;margin:3rem 0 1rem}h2{font-size:2.2rem;font-weight:400;line-height:1.2;margin:3rem 0 1.3rem}a{color:#305c78;text-underline-offset:3px}a:hover{color:#183c55}.repo{font-size:1.15rem}.references{font-size:1.2rem;margin:1.5rem 0;line-height:1.6}nav{margin:2rem 0 3rem}nav ol{padding-left:1.4rem;font-size:1.2rem;line-height:1.7}section{scroll-margin-top:2rem}.text-marker{font:italic 1.15rem/1.6 et-book,Palatino,Georgia,serif;color:#767676;border-left:2px solid #ddd;padding:.5rem 1rem;margin:1.4rem 0 2rem;min-height:3.5rem}.code-box{background:#f8f8f8;border:1px solid #e5e5e5;padding:1rem 1.2rem;margin:1.2rem 0;min-width:0}.source-label{display:none;color:#777;font:11px/1.5 system-ui,sans-serif;letter-spacing:.04em;margin-bottom:.7rem;text-decoration:none}.code-box pre,.code-box code.hl.lean.block{display:block;font:13px/1.65 ui-monospace,SFMono-Regular,Menlo,Consolas,monospace;white-space:pre;overflow-x:auto;max-width:100%;margin:0}.code-box pre+pre{margin-top:1.2rem;padding-top:1rem;border-top:1px solid #ddd}.output{color:#666}.py-keyword{color:#8959a8}.py-function{color:#4271ae}.py-builtin{color:#4271ae}.py-string{color:#718c00}.py-number{color:#c65d09}.py-comment{color:#777;font-style:italic}.py-operator{color:#555}.equation{text-align:center;font:1.4rem/1.8 et-book,Palatino,Georgia,serif;padding:.7rem;overflow-x:auto;white-space:nowrap}figure{margin:2rem 0}figure img{display:block;width:100%;height:auto}details{margin:1.2rem 0}summary{cursor:pointer;font-size:1.2rem;color:#305c78;padding:.6rem 0}.puzzle{border-bottom:1px solid #ddd}.puzzle>summary{font-size:1.5rem;padding:1rem 0}.tippy-box{max-width:min(680px,90vw)!important}.hl.lean .token.binding-hl,.hl.lean .token.typed:hover{background:#eaf3fa}.hl.lean [tabindex]:focus-visible{outline:2px solid #305c78;outline-offset:2px}@media(max-width:650px){body{padding:0 1.2rem 4rem}h1{font-size:2.6rem}h2{font-size:1.9rem}.code-box{padding:.8rem}.code-box pre,.code-box code.hl.lean.block{font-size:12px}nav ol{font-size:1.1rem}.equation{font-size:1.15rem}}@media print{nav{display:none}body{width:100%;padding:0}.code-box{break-inside:avoid}}
/* Expanded goals occupy their own line instead of extending beyond the code cell. */
.code-box .hl.lean .tactic:has(> .tactic-toggle:checked){display:inline}
.code-box .hl.lean .tactic-toggle:checked ~ .tactic-state{display:block;max-width:100%;white-space:pre-wrap;overflow-wrap:anywhere;margin:.6rem 0;font-size:12px}
h3{font-size:1.7rem;font-weight:400;line-height:1.3;margin:2.5rem 0 1rem}
.prose{font-size:1.4rem;line-height:1.5;margin:1.4rem 0;white-space:pre-line}

.prose{white-space:normal}.prose p{margin:1.4rem 0}.prose code{font-size:.8em}.prose pre{overflow-x:auto}

/* Preserve Lean hover markup while letting code fit a phone viewport. */
.code-box pre,
.code-box code.hl.lean.block {
  white-space: pre-wrap;
  overflow-wrap: anywhere;
  tab-size: 2;
}
.code-box code.hl.lean.block .tactic,
.code-box code.hl.lean.block .token {
  white-space: inherit;
}
.source-label { overflow-wrap: anywhere; }
@media (max-width: 650px) {
  body { padding-inline: .8rem; }
  .code-box { padding: .65rem; }
}

/* Keep invisible proof-state controls from widening the document. */
html, body { overflow-x: clip; }