/* verso-archive.css — vendored, not authored.

   The two <style> blocks from the head of the frozen Verso render, concatenated in
   document order and otherwise byte-for-byte as Verso emitted them. Provenance:

     source   harvest/pages/2025-11-1-an-introduction-to-formal-logic.html
     sha256   a00d1d7cf829f528dabed676b87add5f59b50c2b99565af0ffbcc7389c0777b2
     blocks   2244 bytes (:root, --verso-* tokens) + 13869 bytes (rules)
     extracted 2026-08-09

   The same two blocks appear byte-identical in all five harvested pages, checked by
   hashing each — so this is the archive's stylesheet, not one page's.

   Why it is here: `acta assemble --content-root` re-chromes each frozen body by carrying
   the bytes inside its <main> into the new chrome. Those bytes style Lean code as
   `.hl.lean` token spans and tactic states as nested labels, and a page that keeps the
   markup and drops these rules ships unstyled code blocks. The rules live in the content
   repo rather than the engine because engine ⊥ content: acta holds no CSS.

   Do not hand-edit. If it needs to change, change the theme's own sheet after it, which
   is loaded later and wins. The first block below defines `--verso-*` custom properties
   in `:root`, so they are live-tunable in an inspector exactly like the theme's tokens —
   note that they are day-biased (text is `black`) and want overriding under
   phosphor-night. */

:root {
    /** Typography **/
    /* The font family used for headers, ToC entries, etc */
    --verso-structure-font-family: "Helvetica Neue", "Segoe UI", "Roboto", Arial, sans-serif;
    /* The font family used for body text */
    --verso-text-font-family: "Helvetica Neue", "Segoe UI", "Roboto", Arial, sans-serif;
    /* The font family used for code */
    --verso-code-font-family: monospace;

    /** Text colors **/
    --verso-text-color: black;
    --verso-code-color: black;
    --verso-structure-color: black;

    /** Selected items (e.g. search results) */
    --verso-selected-color: #def;

    /** Message colors **/
    /*
    These colors are used to render Lean's feedback. They come in three severities and two
    variants. The raw color itself is used for the text of a message of the indicated severity,
    while the presence of such a message is indicated using the indicator color (e.g. via a
    wavy underline or a bar in the margin).
    */
    --verso-info-color: black;
    --verso-info-indicator-color: #4777ff;
    --verso-warning-color: black;
    --verso-warning-indicator-color: #e7a71d; /* 2.11 contrast ratio for white, 9.94 for black */
    --verso-error-color: #cc0000;
    --verso-error-indicator-color: #ff0000;

    /** Code Highlighting **/
    /*
    These variables control the rendering of Lean code emitted by Verso. Each category that can be
    highlighted supports the customization of color, weight, style, and family.
    */
    /* Constants (e.g. `List` or `id` or `none`) */
    --verso-code-const-color: var(--verso-code-color);
    --verso-code-const-weight: normal;
    --verso-code-const-style: normal;
    --verso-code-const-font-family: var(--verso-code-font-family);

    /* Keywords/atoms (e.g. `for` or `def` or `induction`) */
    --verso-code-keyword-color: var(--verso-code-color);
    --verso-code-keyword-weight: bold;
    --verso-code-keyword-style: normal;
    --verso-code-keyword-font-family: var(--verso-code-font-family);

    /* Local bindings (e.g. `x` in `let x := 5`) */
    --verso-code-var-color: var(--verso-code-color);
    --verso-code-var-weight: normal;
    --verso-code-var-style: italic;
    --verso-code-kw-font-family: var(--verso-code-font-family);
}

/* ---- second block: the rules ---- */

.hl.lean {
  white-space: pre;
  font-weight: normal;
  font-style: normal;
  font-size: inherit;
}

.hl.lean .keyword {
  color: var(--verso-code-keyword-color,);
  font-weight: var(--verso-code-keyword-weight, bold);
  font-style: var(--verso-code-keyword-style, normal);
  font-family: var(--verso-code-keyword-font-family,);
}

.hl.lean .const {
  color: var(--verso-code-const-color,);
  font-weight: var(--verso-code-const-weight, normal);
  font-style: var(--verso-code-const-style, normal);
  font-family: var(--verso-code-const-font-family,);
}

.hl.lean .var {
  color: var(--verso-code-var-color,);
  font-weight: var(--verso-code-var-weight, normal);
  font-style: var(--verso-code-var-style, italic);
  font-family: var(--verso-code-var-font-family,);

  position: relative;
}

.hl.lean .literal, .hl.lean .unknown {
  color: var(--verso-code-color,);
  font-weight: normal;
  font-style: normal;
  font-family: var(--verso-code-font-family,);
}

.hover-container {
  width: 0;
  height: 0;
  position: relative;
  display: inline;
}

.hl.lean a {
  color: inherit;
  text-decoration: currentcolor underline dotted;
}

.hl.lean a:hover {
  text-decoration: currentcolor underline solid;
}

.hl.lean .hover-info {
  white-space: normal;
}

.hl.lean .token .hover-info {
  display: none;
  position: absolute;
  background-color: #e5e5e5;
  border: 1px solid black;
  padding: 0.5rem;
  z-index: 300;
}

.hl.lean .hover-info.messages {
  max-height: 10rem;
  overflow-y: auto;
  overflow-x: hidden;
  scrollbar-gutter: stable;
  padding: 0 0.5rem 0 0;
  display: block;
}

.hl.lean .hover-info code {
  white-space: pre-wrap;
  background: none;
  color: black;
}

.hl.lean .hover-info.messages > code {
  padding: 0.5rem;
  display: block;
  width: fit-content;
}

.hl.lean .hover-info.messages > code:only-child {
  margin: 0;
}

.hl.lean .hover-info.messages > code {
  margin: 0.1rem;
}

.hl.lean .hover-info.messages > code:not(:first-child) {
  margin-top: 0rem;
}

.hl.lean {
}

.hl.lean.block {
  display: block;
}

.hl.lean.inline {
  display: inline;
  white-space: pre-wrap;
}

.hl.lean * {
}

.hl.lean .token {
  transition: all 0.25s; /* Slight fade for highlights */
}

@media (hover: hover) {
  .hl.lean .token.binding-hl, .hl.lean .literal.string:hover, .hl.lean .token.typed:hover {
    background-color: #eee;
    border-radius: 2px;
    transition: none;
  }
}


.hl.lean .has-info .token:not(.tactic-state):not(.tactic-state *), .hl.lean .has-info .inter-text:not(.tactic-state):not(.tactic-state *) {
  text-decoration-style: wavy;
  text-decoration-line: underline;
  text-decoration-thickness: from-font;
  text-decoration-skip-ink: none;
}

.hl.lean .has-info .hover-info {
  display: none;
  position: absolute;
  transform: translate(0.25rem, 0.3rem);
  border: 1px solid black;
  padding: 0.5rem;
  z-index: 400;
  text-align: left;
}

.hl.lean .has-info.error :not(.tactic-state):not(.tactic-state *){
  text-decoration-color: red;
}

@media (hover: hover) {
  .hl.lean .has-info.error:hover {
    background-color: #ffb3b3;
  }
}

.hl.lean .hover-info.messages > code.error {
  background-color: #e5e5e5;
  border-left: 0.2rem solid #ffb3b3;
}

.tippy-box[data-theme~='error'] .hl.lean .hover-info.messages > code.error {
  background: none;
  border: none;
}

.error .verso-message, .error .verso-message .token, .error .verso-message label {
  color: var(--verso-error-color);
}

.error .verso-message .case-label:has(input[type="checkbox"])::before {
  background-color: var(--verso-error-color) !important;
}

.hl.lean .has-info.warning :not(.tactic-state):not(.tactic-state *) {
  text-decoration-color: var(--verso-warning-indicator-color);
}

@media (hover: hover) {
  .hl.lean .has-info.warning:hover {
    background-color:var(--verso-warning-color);
  }
}

.hl.lean .hover-info.messages > code.warning {
  background-color: var(--verso-warning-color);
}

.lean-output {
  border-left: 0.2em solid transparent;
  padding: 0 0 0 0.5em;
  border-top-left-radius: 0;
  border-bottom-left-radius: 0;
}

.lean-output.error {
  border-color: var(--verso-error-indicator-color);
}

.lean-output.information {
  border-color: var(--verso-info-indicator-color);
}

.lean-output.warning {
  border-color: var(--verso-warning-indicator-color);
}

.hl.lean .hover-info.messages > code.error {
  background-color: #e5e5e5;
  border-left: 0.2rem solid var(--verso-warning-color);
}

.tippy-box[data-theme~='warning'] .hl.lean .hover-info.messages > code.warning {
  background: none;
  border: none;
}


.hl.lean .has-info.information :not(.tactic-state):not(.tactic-state *) {
  text-decoration-color: var(--verso-info-indicator-color, blue);
}

@media (hover: hover) {
  .hl.lean .has-info.information:hover {
    background-color: #4777ff;
  }
}


.hl.lean .hover-info.messages > code.information {
  background-color: #e5e5e5;
  border-left: 0.2rem solid #4777ff;
}

.tippy-box[data-theme~='info'] .hl.lean .hover-info.messages > code.information {
  background: none;
  border: none;
}

.hl.lean div.docstring {
  font-family: var(--verso-text-font-family, sans-serif);
  white-space: normal;
  max-width: calc(min(40rem, 90vw));
  width: max-content;
}

.hl.lean div.docstring > :last-child {
  margin-bottom: 0;
}

.hl.lean div.docstring > :first-child {
  margin-top: 0;
}

.hl.lean .hover-info .sep {
  display: block;
  width: auto;
  margin-left: 1rem;
  margin-right: 1rem;
  margin-top: 0.5rem;
  margin-bottom: 0.5rem;
  padding: 0;
  height: 1px;
  border-top: 1px solid #ccc;
}

.hl.lean code {
  font-family: var(--verso-code-font-family);
}

.hl.lean .tactic-state {
  display: none;
  position: relative;
  width: fit-content;
  border: 1px solid #888888;
  border-radius: 0.1rem;
  padding: 0.5rem;
  font-family: sans-serif;
  background-color: #ffffff;
}

.hl.lean.popup .tactic-state {
  position: static;
  display: block;
  width: auto;
  border: none;
  padding: 0.5rem;
  font-family: sans-serif;
  background-color: #ffffff;
}


.hl.lean .tactic {
  position: relative;
  display: inline;
  vertical-align: top;
  /* Without these, mobile Safari will start making font sizes inconsistent when its text size adjustment feature is triggered.*/
  -webkit-text-size-adjust: 100%;
  text-size-adjust: 100%;
}

.hl.lean .tactic:has(.tactic-toggle:checked) {
  display: inline-grid;
  grid-template-columns: 1fr;
}

.hl.lean .tactic-toggle:checked ~ .tactic-state {
  display: inline-block;
  vertical-align: top;
  grid-row: 2;
  justify-self: start;
}

.hl.lean .tactic > label {
  position: relative;
  grid-row: 1;
  display: inline;
}

@media (hover: hover) {
  .hl.lean .tactic:has(.tactic-toggle:not(:checked)) > label:hover {
    background-color: #eeeeee;
  }
}

.hl.lean .tactic-toggle {
  position: absolute;
  top: 0;
  left: 0;
  opacity: 0;
  height: 0;
  width: 0;
  z-index: -10;
}

.hl.lean .tactic > label::after {
  content: "";
  border: 1px solid #bbbbbb;
  /* These need to be em, not rem, to scale with the font */
  border-radius: 1em;
  height: 0.25em;
  vertical-align: middle;
  width: 0.6em;
  margin-left: 0.1em;
  margin-right: 0.1em;
  display: inline-block;
  transition: all 0.5s;
}

/*
@media (hover: hover) {
  .hl.lean .tactic > label:hover::after {
    border: 1px solid #aaaaaa;
    background-color: #aaaaaa;
    transition: all 0.5s;
  }
}
*/

.hl.lean .tactic > label:has(+ .tactic-toggle:checked)::after {
  border: 1px solid #999999;
  background-color: #999999;
  transition: all 0.5s;
}

.hl.lean .tactic-state .goal + .goal {
  margin-top: 1.5em;
}

/*
Some CSS frameworks customize details/summary in ways not compatible with Verso's output.
*/

.hl.lean details {
  display: block !important;
  margin: 0;
}

.hl.lean details summary {
  display: list-item !important;
  margin: 0;
}

.hl.lean details summary:focus {
  outline: none;
  outline-offset: none;
  color: inherit;
}

.hl.lean ul > li {
  margin-bottom: 0;
}

.hl.lean details summary::marker {
  display: inline !important;
}

.hl.lean details > summary:first-of-type {
  list-style-type: disclosure-closed;
  list-style-position: inside;
}

.hl.lean details[open] > summary:first-of-type {
  list-style-type: disclosure-open;
}

.hl.lean details summary::before, .hl.lean details summary::after {
  content: "" !important;
  background: none;
  display: none;
}

.hl.lean .tactic-state summary {
  /* These need to be em, not rem, to scale with the font */
  margin-left: -0.5em;
}

.hl.lean .tactic-state details {
  /* These need to be em, not rem, to scale with the font */
  padding-left: 0.5em;
}

.hl.lean .case-label {
  display: block;
  position: relative;
}

.hl.lean .case-label input[type="checkbox"] {
  position: absolute;
  top: 0;
  left: 0;
  opacity: 0;
  height: 0;
  width: 0;
  z-index: -10;
}

.hl.lean .case-label:has(input[type="checkbox"])::before {
  display: inline-block;
  background-color: black;
  content: ' ';
  transition: ease 0.2s;
  margin-right: 0.7em;
  clip-path: polygon(100% 0, 0 0, 50% 100%);
  width: 0.6em;
  height: 0.6em;
  vertical-align: middle;
}

.hl.lean .case-label:has(input[type="checkbox"]:not(:checked))::before {
  transform: rotate(-90deg);
}

.hl.lean .case-label:has(input[type="checkbox"]) {

}

.hl.lean .case-label:has(input[type="checkbox"]:checked) {

}


.hl.lean .labeled-case > :not(:first-child) {
  max-height: 0px;
  display: block;
  overflow: hidden;
  transition: max-height 0.1s ease-in;
  /* These need to be em, not rem, to scale with the font */
  margin-left: 0.5em;
  margin-top: 0.1em;
}

.hl.lean .labeled-case:has(.case-label input[type="checkbox"]:checked) > :not(:first-child) {
  max-height: 100%;
}


.hl.lean .goal-name::before {
  font-style: normal;
  content: "case ";
}

.hl.lean .goal-name {
  font-style: italic;
  font-family: var(--verso-code-font-family);
  color: inherit;
}

.hl.lean .hypotheses {
  display: table;
}

.hl.lean .hypothesis {
  display: table-row;
}

.hl.lean .hypothesis > * {
  display: table-cell;
}


.hl.lean .hypotheses .colon {
  text-align: center;
  /* This needs to be em, not rem, to scale with the font */
  min-width: 1em;
}

.hl.lean .hypotheses .name {
  text-align: right;
}

.hl.lean .hypotheses .name,
.hl.lean .hypotheses .type,
.hl.lean .conclusion .type {
  font-family: var(--verso-code-font-family);
}

.tippy-box {
  /* Without these, mobile Safari will start making font sizes inconsistent when its text size adjustment feature is triggered.*/
  -webkit-text-size-adjust: 100%;
  text-size-adjust: 100%;

}

.tippy-box[data-theme~='lean'] {
  background-color: #e5e5e5;
  color: black;
  border: 1px solid black;
}
.tippy-box[data-theme~='lean'][data-placement^='top'] > .tippy-arrow::before {
  border-top-color: #e5e5e5;
}
.tippy-box[data-theme~='lean'][data-placement^='bottom'] > .tippy-arrow::before {
  border-bottom-color: #e5e5e5;
}
.tippy-box[data-theme~='lean'][data-placement^='left'] > .tippy-arrow::before {
  border-left-color: #e5e5e5;
}
.tippy-box[data-theme~='lean'][data-placement^='right'] > .tippy-arrow::before {
  border-right-color: #e5e5e5;
}

.tippy-box[data-theme~='message'][data-placement^='top'] > .tippy-arrow::before {
  border-top-color: #e5e5e5;
  border-width: 11px 11px 0;
}
.tippy-box[data-theme~='message'][data-placement^='top'] > .tippy-arrow::after {
  bottom: -11px;
  border-width: 11px 11px 0;
}
.tippy-box[data-theme~='message'][data-placement^='bottom'] > .tippy-arrow::before {
  border-width: 0 11px 11px;
}
.tippy-box[data-theme~='message'][data-placement^='bottom'] > .tippy-arrow::after {
  top: -11px;
  border-width: 0 11px 11px;
}
.tippy-box[data-theme~='message'][data-placement^='left'] > .tippy-arrow::before {
  border-left-color: #e5e5e5;
  border-width: 11px 0 11px 11px;
}
.tippy-box[data-theme~='message'][data-placement^='left'] > .tippy-arrow::after {
  right: -11px;
  border-width: 11px 0 11px 11px;
}

.tippy-box[data-theme~='message'][data-placement^='right'] > .tippy-arrow::before {
  border-right-color: #e5e5e5;
  border-width: 11px 11px 11px 0;
}
.tippy-box[data-theme~='message'][data-placement^='right'] > .tippy-arrow::after {
  left: -11px;
  border-width: 11px 11px 11px 0;
}



.tippy-box[data-theme~='warning'] {
  background-color: #e5e5e5;
  color: black;
  border: 3px solid var(--verso-warning-color);
}

.tippy-box[data-theme~='error'] {
  background-color: #e5e5e5;
  color: black;
  border: 3px solid #f7a7af;
}

.tippy-box[data-theme~='info'] {
  background-color: #e5e5e5;
  color: black;
  border: 3px solid #99b3c2;
}

.tippy-box[data-theme~='tactic'] {
  background-color: white;
  color: black;
  border: 1px solid black;
}
.tippy-box[data-theme~='tactic'][data-placement^='top'] > .tippy-arrow::before {
  border-top-color: white;
}
.tippy-box[data-theme~='tactic'][data-placement^='bottom'] > .tippy-arrow::before {
  border-bottom-color: white;
}
.tippy-box[data-theme~='tactic'][data-placement^='left'] > .tippy-arrow::before {
  border-left-color: white;
}
.tippy-box[data-theme~='tactic'][data-placement^='right'] > .tippy-arrow::before {
  border-right-color: white;
}

.extra-doc-links {
  list-style-type: none;
  margin-left: 0;
  padding: 0;
}

.extra-doc-links > li {
  display: inline-block;
}

.extra-doc-links > li:not(:last-child)::after {
  content: '|';
  display: inline-block;
  margin: 0 0.25em;
}

.verso-message .trace {
  display: block;
}

.verso-message .trace > summary::marker {
  color: var(--verso-text-color);
}

.verso-message .trace-children {
  margin: 0;
  padding: 0;
}

.verso-message .trace-children > li {
  list-style-type: none;
  margin-left: 1.5em;
}

.verso-message .trace-children > li:not(:has(.trace)) {
  margin-left: 0;
}

.verso-message .trace-class {
  color: color-mix(in srgb, currentColor 70%, transparent);
  font-weight: bold;
  margin: 0;
  padding: 0;
}

.verso-message .text {
  white-space: pre-wrap;
}