.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,);
}

/* These lexically-classified token kinds default to the `.unknown` appearance. The rule follows
   `.const` so it wins for the `anon-ctor` tokens, which also carry the `const` class. */
.hl.lean .anon-ctor,
.hl.lean .number,
.hl.lean .char,
.hl.lean .comment,
.hl.lean .punctuation,
.hl.lean .delim,
.hl.lean .wildcard {
  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;
}

/* Links inside tooltips show their underline only when hovered. */
.tippy-box .hl.lean a {
  text-decoration: none;
}

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

.hl.lean .token .hover-info {
  display: none;
  position: absolute;
  color: var(--verso-tooltip-color, black);
  background-color: var(--verso-tooltip-bg-color, #e5e5e5);
  border: 1px solid var(--verso-tooltip-border-color, 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;
}

.hl.lean .hover-info code:not(.verso-message) {
  color: var(--verso-tooltip-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) {
  /* Hovered content nested in a collapsed tactic region keeps its plain background: the
     region's proof state is the tooltip that appears there, and its label is what
     highlights. `:where` keeps the exclusion out of the specificity computation. */
  .hl.lean .token.binding-hl,
  .hl.lean :is(.literal, .token.typed, .token[data-verso-hover]):hover:not(:where(.tactic:has(> .tactic-toggle:not(:checked)) > label *)) {
    background-color: var(--verso-code-hover-bg-color, #eeeeee);
    border-radius: 2px;
    transition: none;
  }

  /* Within a hovered message span, token hover backgrounds are removed so the span's own
     hover background shows across the whole span. The exception is a hovered documented
     token, which keeps its background because its tooltip is the one shown. */
  .hl.lean .has-info:hover .token.binding-hl:not(:hover),
  .hl.lean .has-info:hover .token.binding-hl:not([data-verso-hover]),
  .hl.lean .has-info:hover .literal:hover:not([data-verso-hover]),
  .hl.lean .has-info:hover .token.typed:hover:not([data-verso-hover]) {
    background-color: transparent;
  }
}


.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;
}

/*
The underline color comes from the nearest enclosing message span: each severity's span rule
sets `--verso--region-indicator-color`, which inherits, so a region nested inside one of
another severity keeps its own indicator color.
*/
.hl.lean .has-info :not(.tactic-state):not(.tactic-state *) {
  text-decoration-color: var(--verso--region-indicator-color);
}

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

.hl.lean .has-info.error {
  --verso--region-indicator-color: var(--verso-error-indicator-color, #ff0000);
  --verso--region-hover-color: var(--verso-code-error-hover-color, currentcolor);
  --verso--region-hover-bg-color: var(--verso-code-error-hover-bg-color, #ffb3b3);
  color: var(--verso-code-error-color, currentcolor);
  background-color: var(--verso-code-error-bg-color, transparent);
}

/*
The hover highlight follows the tooltip: a message span highlights only when its own tooltip
is the one that appears. When a hovered nested message span, a hovered documented token, or
a hovered collapsed tactic label shows its own tooltip instead, the message span does not
highlight. A span nested in a collapsed tactic region likewise stays plain, because hovering
it shows the region's proof state; `:where` keeps that exclusion out of the specificity
computation.

The hover colors come from `--verso--region-hover-color` and `--verso--region-hover-bg-color`,
which each severity's span rule sets. This keeps the hover conditions in this one rule, and
because the properties inherit, a region nested inside one of another severity keeps its own
hover colors.
*/
@media (hover: hover) {
  .hl.lean .has-info:hover:not(:has(.has-info:hover)):not(:has([data-verso-hover]:hover)):not(:has(.tactic > label:hover + .tactic-toggle:not(:checked))):not(:where(.tactic:has(> .tactic-toggle:not(:checked)) > label *)) {
    color: var(--verso--region-hover-color, currentcolor);
    background-color: var(--verso--region-hover-bg-color, transparent);
  }
}

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

/*
A tooltip that shows only messages of the box's own severity leaves severity styling to the
box itself. When messages of several severities share the tooltip, or a `mixed` tooltip
combines messages with other content (such as documentation), each message keeps its
severity accent to distinguish them.
*/
.tippy-box .hl.lean.mixed > .hover-info.messages {
  margin-bottom: 0.5rem;
}

.tippy-box[data-theme~='error'] .hl.lean:not(.mixed) .hover-info.messages:not(:has(> code.warning)):not(:has(> code.information)) > code.error {
  background: none;
  border: none;
}

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

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

.hl.lean .has-info.warning {
  --verso--region-indicator-color: var(--verso-warning-indicator-color, #e7a71d);
  --verso--region-hover-color: var(--verso-code-warning-hover-color, currentcolor);
  --verso--region-hover-bg-color: var(--verso-code-warning-hover-bg-color, #ffd580);
  color: var(--verso-code-warning-color, currentcolor);
  background-color: var(--verso-code-warning-bg-color, transparent);
}

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

.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-output-error-color, var(--verso-error-indicator-color, #ff0000));
}

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

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

.tippy-box[data-theme~='warning'] .hl.lean:not(.mixed) .hover-info.messages:not(:has(> code.error)):not(:has(> code.information)) > code.warning {
  background: none;
  border: none;
}

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

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


.hl.lean .has-info.information {
  --verso--region-indicator-color: var(--verso-info-indicator-color, #4777ff);
  --verso--region-hover-color: var(--verso-code-info-hover-color, currentcolor);
  --verso--region-hover-bg-color: var(--verso-code-info-hover-bg-color, #4777ff);
  color: var(--verso-code-info-color, currentcolor);
  background-color: var(--verso-code-info-bg-color, transparent);
}


.hl.lean .hover-info.messages > code.information {
  background-color: var(--verso-tooltip-info-bg-color, #e5e5e5);
  border-left: 0.2rem solid var(--verso-tooltip-info-border-color, #4777ff);
}

.tippy-box[data-theme~='info'] .hl.lean:not(.mixed) .hover-info.messages:not(:has(> code.error)):not(:has(> code.warning)) > code.information {
  background: none;
  border: none;
}

.information .verso-message, .information .verso-message .token, .information .verso-message label {
  color: var(--verso-message-info-color, black);
}

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

.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 var(--verso-tooltip-separator-color, #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 var(--verso-tactic-state-border-color, #888888);
  border-radius: 0.1rem;
  padding: 0.5rem;
  font-family: sans-serif;
  color: var(--verso-tactic-state-color, black);
  background-color: var(--verso-tactic-state-bg-color, white);
}

.hl.lean.popup .tactic-state {
  position: static;
  display: block;
  width: auto;
  border: none;
  padding: 0.5rem;
  font-family: sans-serif;
  background-color: var(--verso-tactic-state-bg-color, white);
}


.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) {
  /* Highlight a region on hover only when its own toggle is unchecked, and only the innermost
     hovered region: `label:hover` bubbles to ancestor labels, so suppress the highlight on a region
     whose label contains a more deeply nested hovered tactic label. The region's proof state is the
     tooltip for everything else in its label, so the label keeps its highlight while any of that
     content is hovered. */
  .hl.lean .tactic:has(> .tactic-toggle:not(:checked)) > label:hover:not(:has(.tactic > label:hover)) {
    background-color: var(--verso-code-hover-bg-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 var(--verso-tactic-toggle-color, #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 var(--verso-tactic-toggle-checked-color, #999999);
  background-color: var(--verso-tactic-toggle-checked-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: currentcolor;
  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's stylesheet paints each arrow's fill triangle with the arrow element's `color` (its
placement-specific `::before` rules use `border-color: initial`, which is `currentcolor`),
and its border extension paints the outline triangle with the box's border color. Setting
`color` on the arrow therefore matches it to the tooltip background for every placement.
*/
.tippy-box[data-theme~='lean'] {
  background-color: var(--verso-tooltip-bg-color, #e5e5e5);
  color: var(--verso-tooltip-color, black);
  border: 1px solid var(--verso-tooltip-border-color, black);
}
.tippy-box[data-theme~='lean'] > .tippy-arrow {
  color: var(--verso-tooltip-bg-color, #e5e5e5);
}

.tippy-box[data-theme~='message'][data-placement^='top'] > .tippy-arrow::before {
  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-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-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: var(--verso-tooltip-warning-bg-color, #e5e5e5);
  color: var(--verso-tooltip-warning-color, black);
  border: 3px solid var(--verso-tooltip-warning-border-color, #ffd580);
}
.tippy-box[data-theme~='warning'] > .tippy-arrow {
  color: var(--verso-tooltip-warning-bg-color, #e5e5e5);
}

.tippy-box[data-theme~='error'] {
  background-color: var(--verso-tooltip-error-bg-color, #e5e5e5);
  color: var(--verso-tooltip-error-color, black);
  border: 3px solid var(--verso-tooltip-error-border-color, #ffb3b3);
}
.tippy-box[data-theme~='error'] > .tippy-arrow {
  color: var(--verso-tooltip-error-bg-color, #e5e5e5);
}

.tippy-box[data-theme~='info'] {
  background-color: var(--verso-tooltip-info-bg-color, #e5e5e5);
  color: var(--verso-tooltip-info-color, black);
  border: 3px solid var(--verso-tooltip-info-border-color, #4777ff);
}
.tippy-box[data-theme~='info'] > .tippy-arrow {
  color: var(--verso-tooltip-info-bg-color, #e5e5e5);
}

.tippy-box[data-theme~='tactic'] {
  background-color: var(--verso-tactic-state-bg-color, white);
  color: var(--verso-tactic-state-color, black);
  border: 1px solid var(--verso-tactic-state-border-color, #888888);
}
.tippy-box[data-theme~='tactic'] > .tippy-arrow {
  color: var(--verso-tactic-state-bg-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, black);
}

.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;
}