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