@import url('https://cdnjs.cloudflare.com/ajax/libs/lato-font/3.0.0/css/lato-font.min.css');
@import url('https://cdnjs.cloudflare.com/ajax/libs/juliamono/0.051/juliamono.css');

* {
    box-sizing: border-box;
}

body {
    font-size: 17px;
    font-variant-ligatures: none;
    font-family: 'Lato Medium';
    color: var(--text-color);
    background: var(--body-bg);
}

input, select, textarea, button{font-family:inherit;}

a {
   color: var(--link-color);
}

h1, h2, h3, h4, h5, h6 {
    font-family: 'Lato Medium';
}

body { line-height: 1.5; }
nav { line-height: normal; }

:root {
    --header-height: 3em;
    --fragment-offset: calc(var(--header-height) + 1em);
    --content-width: 55vw;

    --header-bg: #f8f8f8;
    --body-bg: white;
    --code-bg: #f3f3f3;
    --text-color: black;
    --link-color: hsl(210, 100%, 30%);

    --implicit-arg-text-color: var(--text-color);

    --def-color: #92dce5;
    --def-color-hsl-angle: 187;
    --theorem-color: #8fe388;
    --theorem-color-hsl-angle: 115;
    --axiom-and-constant-color: #f44708;
    --axiom-and-constant-color-hsl-angle: 16;
    --structure-and-inductive-color: #f0a202;
    --structure-and-inductive-color-hsl-angle: 40;
    --starting-percentage: 100;

    --hamburger-bg-color: #eee;
    --hamburger-active-color: white;
    --hamburger-border-color: #ccc;

    --tags-border-color: #555;

    --fragment-offset: calc(var(--header-height) + 1em);
    --content-width: 55vw;
}
/* automatic dark theme if no javascript */
@media (prefers-color-scheme: dark) {
    :root {
        --header-bg: #111010;
        --body-bg: #171717;
        --code-bg: #363333;
        --text-color: #eee;
        --link-color: #58a6ff;

        --implicit-arg-text-color: var(--text-color);

        --def-color: #1F497F;
        --def-color-hsl-angle: 214;
        --theorem-color: #134E2D;
        --theorem-color-hsl-angle: 146;
        --axiom-and-constant-color: #6B1B1A;
        --axiom-and-constant-color-hsl-angle: 1;
        --structure-and-inductive-color: #73461C;
        --structure-and-inductive-color-hsl-angle: 29;
        --starting-percentage: 30;

        --hamburger-bg-color: #2d2c2c;
        --hamburger-active-color: black;
        --hamburger-border-color: #717171;

        --tags-border-color: #AAA;
    }
}

[data-theme="light"] {
    color-scheme: light;

    --header-height: 3em;
    --fragment-offset: calc(var(--header-height) + 1em);
    --content-width: 55vw;

    --header-bg: #f8f8f8;
    --body-bg: white;
    --code-bg: #f3f3f3;
    --text-color: black;
    --link-color: hsl(210, 100%, 30%);

    --implicit-arg-text-color: var(--text-color);

    --def-color: #92dce5;
    --def-color-hsl-angle: 187;
    --theorem-color: #8fe388;
    --theorem-color-hsl-angle: 115;
    --axiom-and-constant-color: #f44708;
    --axiom-and-constant-color-hsl-angle: 16;
    --structure-and-inductive-color: #f0a202;
    --structure-and-inductive-color-hsl-angle: 40;
    --starting-percentage: 100;

    --hamburger-bg-color: #eee;
    --hamburger-active-color: white;
    --hamburger-border-color: #ccc;

    --tags-border-color: #555;

    --fragment-offset: calc(var(--header-height) + 1em);
    --content-width: 55vw;
}

[data-theme="dark"] {
    color-scheme: dark;

    --header-bg: #111010;
    --body-bg: #171717;
    --code-bg: #363333;
    --text-color: #eee;
    --link-color: #58a6ff;

    --implicit-arg-text-color: var(--text-color);

    --def-color: #1F497F;
    --def-color-hsl-angle: 214;
    --theorem-color: #134E2D;
    --theorem-color-hsl-angle: 146;
    --axiom-and-constant-color: #6B1B1A;
    --axiom-and-constant-color-hsl-angle: 1;
    --structure-and-inductive-color: #73461C;
    --structure-and-inductive-color-hsl-angle: 29;
    --starting-percentage: 30;

    --hamburger-bg-color: #2d2c2c;
    --hamburger-active-color: black;
    --hamburger-border-color: #717171;

    --tags-border-color: #AAA;
}

@supports (width: min(10px, 5vw)) {
    :root {
        --content-width: clamp(20em, 55vw, 60em);
    }
}

#nav_toggle {
    display: none;
}
label[for="nav_toggle"] {
    display: none;
}

header {
    height: var(--header-height);
    float: left;
    position: fixed;
    width: 100vw;
    max-width: 100%;
    left: 0;
    right: 0;
    top: 0;
    --header-side-padding: 1em;
    padding: 0 var(--header-side-padding);
    background: var(--header-bg);
    z-index: 1;
    display: flex;
    align-items: center;
    justify-content: space-between;
}

@media screen and (max-width: 1000px) {
    :root {
        --content-width: 100vw;
    }

    .internal_nav {
        display: none;
    }

    body .nav {
        width: 100vw;
        max-width: 100vw;
        margin-left: 1em;
        z-index: 1;
    }

    body main {
        width: unset;
        max-width: unset;
        margin-left: unset;
        margin-right: unset;
    }
    body .decl > div {
        overflow-x: unset;
    }

    #nav_toggle:not(:checked) ~ .nav {
        display: none;
    }
    #nav_toggle:checked ~ main {
        visibility: hidden;
    }

    label[for="nav_toggle"]::before {
        content: '≡';
    }
    label[for="nav_toggle"] {
        display: inline-block;
        margin-right: 1em;
        border: 1px solid var(--hamburger-border-color);
        padding: 0.5ex 1ex;
        cursor: pointer;
        background: var(--hamburger-bg-color);
    }
    #nav_toggle:checked ~ * label[for="nav_toggle"] {
        background: var(--hamburger-active-color);
    }

    body header h1 {
        font-size: 100%;
    }

    header {
        --header-side-padding: 1ex;
    }
}
@media screen and (max-width: 700px) {
    header h1 span { display: none; }
    :root { --header-side-padding: 1ex; }
    #search_form button { display: none; }
    #search_form input { width: 100%; }
    header #autocomplete_results {
        left: 1ex;
        right: 1ex;
        width: inherit;
    }
    body header > * { margin: 0; }
}

header > * {
    display: inline-block;
    padding: 0;
    margin: 0;
    vertical-align: middle;
}

header h1 {
    font-weight: normal;
    font-size: 1.5em;
}

header .header_filename {
    font-size: 17px;
    color: gray;
    text-align: center;
    line-height: 95%;
}

/* inserted by nav.js */
#autocomplete_results {
    position: absolute;
    top: var(--header-height);
    right: calc(var(--header-side-padding));
    width: calc(20em + 4em);
    z-index: 1;
    background: var(--header-bg);
    border: 1px solid #aaa;
    border-top: none;
    overflow-x: hidden;
    overflow-y: auto;
    max-height: calc(100vh - var(--header-height));
}

#autocomplete_results:empty {
    display: none;
}

#autocomplete_results[state="loading"]:empty {
    display: block;
    cursor: progress;
}
#autocomplete_results[state="loading"]:empty::before {
    display: block;
    content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 ';
    padding: 1ex;
    animation: marquee 10s linear infinite;
}
@keyframes marquee {
    0% { transform: translate(100%, 0); }
    100% { transform: translate(-100%, 0); }
}

#autocomplete_results[state="done"]:empty {
    display: block;
    text-align: center;
    padding: 1ex;
}
#autocomplete_results[state="done"]:empty::before {
    content: '(no results)';
    font-style: italic;
}

#autocomplete_results a {
    display: block;
    color: inherit;
    padding: 1ex;
    border-left: 0.5ex solid transparent;
    padding-left: 0.5ex;
    cursor: pointer;
}

#autocomplete_results .selected .result_link a {
    background: var(--body-bg);
    border-color: var(--structure-and-inductive-color);
}


#search_results {
    width: 100%;
}
#search_results[state="done"]:empty::before {
    content: '(no results)';
    font-style: italic;
}

#search_results .result_link, #search_results .result_doc {
    border-bottom: 1px solid rgba(0, 0, 0, 0.8);
}

.search_result_block {
    width: 100%;
    content-visibility: auto;
    contain-intrinsic-size: auto 75em;
}

.search_result_block_inner {
    display: table;
    width: 100%;
}

.search_result {
    display: table-row;
}

.result_link, .result_doc {
    display: table-cell;
    overflow: hidden;
    word-break: break-word;
}

main, nav {
    margin-top: calc(var(--header-height) + 1em);
}

/* extra space for scrolling things to the top */
main {
    margin-bottom: 90vh;
}

main {
    max-width: var(--content-width);
    /* center it: */
    margin-left: auto;
    margin-right: auto;
}

nav {
    float: left;
    height: calc(100vh - var(--header-height) - 1em);
    position: fixed;
    top: 0;
    overflow: auto;
    scrollbar-width: thin;
    scrollbar-color: transparent transparent;
}

nav:hover {
    scrollbar-color: gray transparent;
}

nav {
    --column-available-space: calc((100vw - var(--content-width) - 5em)/2);
    --column-width: calc(var(--column-available-space) - 1ex);
    --dist-to-edge: 1ex;
    width: var(--content-width);
    max-width: var(--column-width);
}
@supports (width: min(10px, 5vw)) {
    .nav { --desired-column-width: 20em; }
    .internal_nav { --desired-column-width: 30em; }
    nav {
        --column-available-space: calc(max(0px, (100vw - var(--content-width) - 5em)/2));
        --column-width: calc(clamp(0px, var(--column-available-space) - 1ex, var(--desired-column-width)));
        --dist-to-edge: calc(max(1ex, var(--column-available-space) - var(--column-width)));
    }
}

.nav { left: var(--dist-to-edge); }
.internal_nav { right: var(--dist-to-edge); }

.internal_nav .nav_link, .taclink {
    /* indent everything but first line by 2ex */
    text-indent: -2ex; padding-left: 2ex;
}

.navframe {
    height: 100%;
    width: 100%;
}

.navframe .nav {
    position: absolute;
    left: 0;
    margin-left: 0;
}

.internal_nav .imports {
    margin-bottom: 1rem;
}

.tagfilter-div {
    margin-bottom: 1em;
}
.tagfilter-div > summary {
    margin-bottom: 1ex;
}

/* top-level modules in left navbar */
.nav .module_list > details {
    margin-top: 1ex;
}

.nav details > * {
    padding-left: 2ex;
}

.nav summary {
    cursor: pointer;
    padding-left: 0;
}

.nav summary::marker {
    font-size: 85%;
}

.nav .nav_file {
    display: inline-block;
}

.nav h3 {
    margin-block-end: 4px;
}

/* People use way too long declaration names. */
.internal_nav, .decl_name {
    overflow-wrap: break-word;
}

/* Add a linebreak after a declaration name. */
.decl_name::after {
    content: "\A";
    white-space: pre;
}

.nav_link {
    overflow-wrap: break-word;
}

.navframe {
    --header-height: 0;
}

#settings {
    margin-top: 5em;
}
#settings h3 {
    font-size: inherit;
}

#color-theme-switcher {
    display: flex;
    justify-content: space-between;
    padding: 0 2ex;
    flex-flow: row wrap;
}

/* custom radio buttons for dark/light switch */
#color-theme-switcher input {
    -webkit-appearance: none;
    -moz-appearance: none;
    appearance: none;
    display: inline-block;
    box-sizing: content-box;
    height: 1em;
    width: 1em;
    background-clip: content-box;
    padding: 2px;
    border: 2px solid transparent;
    margin-bottom: -4px;
    border-radius: 50%;
}
#color-theme-dark { background-color: #444; }
#color-theme-light { background-color: #ccc; }
#color-theme-system {
    background-image: linear-gradient(60deg, #444, #444 50%, #CCC 50%, #CCC);
}
#color-theme-switcher input:checked {
    border-color: var(--text-color);
}

.decl > div, .mod_doc {
    padding-left: 8px;
    padding-right: 8px;
}

.decl {
    margin-top: 20px;
    margin-bottom: 20px;
}

.decl > div {
    /* sometimes declarations arguments are way too long
       and would continue into the right column,
       so put a scroll bar there: */
    overflow-x: auto;
}

/* Make `#id` links appear below header. */
.decl, h1[id], h2[id], h3[id], h4[id], h5[id], h6[id] {
    scroll-margin-top: var(--fragment-offset);
}
/* don't need as much vertical space for these
inline elements */
a[id], li[id] {
    scroll-margin-top: var(--header-height);
}

/* HACK: Safari doesn't support scroll-margin-top for
fragment links (yet?)
https://caniuse.com/mdn-css_properties_scroll-margin-top
https://bugs.webkit.org/show_bug.cgi?id=189265
*/
@supports not (scroll-margin-top: var(--fragment-offset)) {
    .decl::before, h1[id]::before, h2[id]::before, h3[id]::before,
    h4[id]::before, h5[id]::before, h6[id]::before,
    a[id]::before, li[id]::before {
        content: "";
        display: block;
        height:      var(--fragment-offset);
        margin-top:  calc(-1 * var(--fragment-offset));
        box-sizing: inherit;
        visibility: hidden;
        width: 1px;
    }
}


/* hide # after markdown headings except on hover */
.markdown-heading:not(:hover) > .hover-link {
    visibility: hidden;
}

main h2, main h3, main h4, main h5, main h6 {
    margin-top: 1rem;
    margin-bottom: -0.4rem;
}
.decl + .mod_doc > h2,
        .decl + .mod_doc > h3,
        .decl + .mod_doc > h4,
        .decl + .mod_doc > h5,
        .decl + .mod_doc > h6 {
    margin-top: 4rem;
}

.def, .instance {
    border-left: 10px solid var(--text-color);
    border-top: 2px solid var(--text-color);
}

.theorem {
    border-left: 10px solid var(--theorem-color);
    border-top: 2px solid var(--theorem-color);
}

.axiom, .opaque {
    border-left: 10px solid var(--axiom-and-constant-color);
    border-top: 2px solid var(--axiom-and-constant-color);
}

.structure, .inductive, .class {
    border-left: 10px solid var(--structure-and-inductive-color);
    border-top: 2px solid var(--structure-and-inductive-color);
}

.fn {
    display: inline-block;
    /* border: 1px dashed red; */
    text-indent: -1ex;
    padding-left: 1ex;
    white-space: pre-wrap;
    vertical-align: top;
}

.fn { --fn: 1; }
.fn .fn { --fn: 2; }
.fn .fn .fn { --fn: 3; }
.fn .fn .fn .fn { --fn: 4; }
.fn .fn .fn .fn .fn { --fn: 5; }
.fn .fn .fn .fn .fn .fn { --fn: 6; }
.fn .fn .fn .fn .fn .fn .fn { --fn: 7; }
.fn .fn .fn .fn .fn .fn .fn .fn { --fn: 8; }
.fn {
    transition: background-color 100ms ease-in-out;
}

.def .fn:hover, .instance .fn:hover {
    background-color: hsla(var(--def-color-hsl-angle), 61%, calc(var(--starting-percentage) - 5%*var(--fn)));
    box-shadow: 0 0 0 1px hsla(var(--def-color-hsl-angle), 61%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
    border-radius: 5px;
}
.theorem .fn:hover {
    background-color: hsla(var(--theorem-color-hsl-angle), 62%, calc(var(--starting-percentage) - 5%*var(--fn)));
    box-shadow: 0 0 0 1px hsla(var(--theorem-color-hsl-angle), 62%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
    border-radius: 5px;
}
.axiom .fn:hover, .opaque .fn:hover {
    background-color: hsla(var(--axiom-and-constant-color-hsl-angle), 94%, calc(var(--starting-percentage) - 5%*var(--fn)));
    box-shadow: 0 0 0 1px hsla(var(--axiom-and-constant-color-hsl-angle), 94%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
    border-radius: 5px;
}
.structure .fn:hover, .inductive .fn:hover, .class .fn:hover {
    background-color: hsla(var(--structure-and-inductive-color-hsl-angle), 98%, calc(var(--starting-percentage) - 5%*var(--fn)));
    box-shadow: 0 0 0 1px hsla(var(--structure-and-inductive-color-hsl-angle), 98%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
    border-radius: 5px;
}

.decl_args, .decl_type .decl_parent {
    font-weight: normal;
}

.implicits, .impl_arg {
    color: var(--text-color);
    white-space: normal;
}

.decl_kind, .decl_name, .decl_extends {
    font-weight: bold;
}

/* break long declaration names at periods where possible */
.break_within {
    word-break: break-all;
}

.break_within .name {
    word-break: normal;
}

.decl_header {
    /* indent everything but first line twice as much as decl_type */
    text-indent: -8ex; padding-left: 8ex;
}

.decl_type {
    margin-top: 2px;
    margin-left: 4ex; /* extra indentation */
}

.decl.sorried .decl_name {
    text-decoration: underline wavy #cca733;
}

.decl .sorry_msg > strong {
    color: #a90000;
}

.imports li, code, .decl_header, .attributes, .structure_field_info,
        .constructor, .instances li, .instances-for-list li, .equation, .structure_ext_ctor {
    font-size: 92%;
    font-family: 'JuliaMono', monospace;
}

pre {
    white-space: break-spaces;
}

code, pre { background: var(--code-bg); }
code, pre { border-radius: 5px; }
code { padding: 1px 3px; }
pre { padding: 1ex; }
pre code { padding: 0 0; }

#howabout code { background: inherit; }
#howabout li { margin-bottom: 0.5ex; }

.structure_fields, .constructors {
    display: block;
    padding-inline-start: 0;
    margin-top: 1ex;
    text-indent: -2ex; padding-left: 2ex;
}

.structure_field {
    display: block;
    margin-left: 2ex;
}

.inductive_ctor_doc  {
    text-indent: 0;
    margin-left: 2ex;
    font-family: 'Lato Medium';
    font-size: 17px;
}

.structure_field_doc {
    text-indent: 0;
    font-family: 'Lato Medium';
    font-size: 17px;
}

.structure_ext_fields {
    display: block;
    padding-inline-start: 0;
    margin-top: 1ex;
    text-indent: -2ex; padding-left: 2ex;
}

.structure_ext_fields .structure_field {
    margin-left: -1ex !important;
}

.structure_ext_ctor {
    display: block;
    text-indent: -3ex;
}

.constructor {
    display: block;
}
.constructor:before {
    content: '| ';
    color: gray;
}

/** Don't show underline on types, to prevent the ≤ vs < confusion. **/
a:link, a:visited, a:active {
    color:var(--link-color);
    text-decoration: none;
}

/** Show it on hover though. **/
a:hover {
    text-decoration: underline;
}

.impl_arg {
    font-style: italic;
    transition: opacity 300ms ease-in;
}

.decl_header:not(:hover) .impl_arg,
        .constructor:not(:hover) .impl_arg,
        .structure_field_info:not(:hover) .impl_arg {
    opacity: 30%;
    transition: opacity 1000ms ease-out;
}

.inherited_field {
    transition: opacity 300ms ease-in;
}

.structure_fields:not(:hover) .inherited_field {
    opacity: 30%;
    transition: opacity 1000ms ease-out;
}

.gh_link {
    float: right;
    margin-left: 10px;
}

.ink_link {
    float: right;
    margin-left: 20px;
}


.docfile h2, .note h2 {
    margin-block-start: 3px;
    margin-block-end: 0px;
}

.docfile h2 a {
    color: var(--text-color);
}

.tags {
    margin-bottom: 1ex;
}

.tags ul {
    display: inline;
    padding: 0;
}

.tags li {
    border: 1px solid var(--tags-border-color);
    border-radius: 4px;
    list-style-type: none;
    padding: 1px 3px;
    margin-left: 1ex;
    display: inline-block;
}

/* used by nav.js */
.hide { display: none; }

.tactic, .note {
    border-top: 3px solid #0479c7;
    padding-top: 2em;
    margin-top: 2em;
    margin-bottom: 2em;
}


/* TorchLean public docs polish */

/* Shared polish variables -------------------------------------------------
   DocGen already defines semantic colors for declaration kinds.  These
   TorchLean variables cover site chrome: teal accents, soft borders, and
   shadows used by the landing page and sidebar cards. */
header h1 span {
  letter-spacing: 0;
}

:root {
  --tl-teal: #157878;
  --tl-teal-soft: rgba(21, 120, 120, 0.13);
  --tl-border: rgba(17, 44, 64, 0.16);
  --tl-shadow: 0 16px 44px rgba(17, 44, 64, 0.08);
  --content-width: clamp(36rem, 64vw, 78rem);
}

html,
body {
  max-width: 100%;
  overflow-x: hidden;
}

body {
  font-size: 18px;
  background:
    radial-gradient(circle at top left, color-mix(in srgb, var(--code-bg) 35%, transparent), transparent 28rem),
    var(--body-bg);
}

/* Header and search -------------------------------------------------------
   Keep DocGen's fixed header model, but make it feel like the rest of the
   public site.  Search remains the real DocGen search form. */
header {
  border-bottom: 1px solid rgba(127, 127, 127, 0.18);
  box-shadow: 0 8px 28px rgba(17, 44, 64, 0.06);
  backdrop-filter: blur(10px);
}

header h1 {
  display: flex;
  align-items: center;
  gap: 0.35rem;
  min-width: 0;
}

header .header_filename {
  color: color-mix(in srgb, var(--text-color) 66%, transparent);
  font-size: 0.92rem;
  min-width: 0;
}

#search_form {
  white-space: nowrap;
}

#search_form input,
#search_page_query {
  border: 1px solid rgba(127, 127, 127, 0.28);
  border-radius: 999px;
  padding: 0.42rem 0.72rem;
  background: color-mix(in srgb, var(--body-bg) 92%, var(--code-bg));
  color: var(--text-color);
}

#search_button {
  border: 1px solid var(--tl-border);
  border-radius: 999px;
  padding: 0.38rem 0.72rem;
  background: var(--tl-teal);
  color: white;
  cursor: pointer;
}

#search_button:hover {
  filter: brightness(0.94);
}

/* Cross-site links --------------------------------------------------------
   Generated API pages sit under `/docs/`, while the human guide and examples
   sit elsewhere in the Jekyll site.  These links prevent the docs from feeling
   like a dead-end generated artifact. */
.tl-docsite-links {
  display: flex;
  align-items: center;
  gap: 0.35rem;
  font-size: 0.86rem;
}

.tl-docsite-links a {
  color: color-mix(in srgb, var(--text-color) 78%, transparent);
  text-decoration: none;
  padding: 0.24rem 0.48rem;
  border-radius: 999px;
}

.tl-docsite-links a:hover {
  color: var(--tl-teal);
  background: var(--tl-teal-soft);
  text-decoration: none;
}

/* Landing-page module drawer ---------------------------------------------
   The landing page uses the same hidden checkbox / iframe navbar that DocGen
   emits everywhere else. The custom index hides the drawer by default and
   expose it with a human label, "Modules", instead of the raw hamburger glyph. */
.tl-docs-index {
  --content-width: min(1080px, calc(100vw - 3rem));
}

.tl-docs-index header {
  justify-content: flex-start;
  gap: 1rem;
}

.tl-docs-index #search_form {
  margin-left: auto;
}

.tl-docs-index .header_filename {
  display: none;
}

.tl-docs-index .nav {
  display: none;
}

.tl-docs-index #nav_toggle:checked ~ .nav {
  display: block;
  width: min(24rem, calc(100vw - 2rem));
  max-width: none;
  left: 1rem;
  z-index: 4;
  background: var(--body-bg);
  border: 1px solid rgba(127, 127, 127, 0.24);
  border-radius: 12px;
  padding: 0.75rem;
}

.tl-docs-index label[for="nav_toggle"] {
  display: inline-block;
  margin-right: 0.5rem;
  border: 1px solid var(--hamburger-border-color);
  padding: 0.25rem 0.62rem;
  cursor: pointer;
  background: var(--hamburger-bg-color);
  border-radius: 999px;
}

.tl-docs-index label[for="nav_toggle"]::before {
  content: 'Modules';
}

/* Landing-page layout -----------------------------------------------------
   These rules are only for `/docs/`: a hero, entrypoint cards, layer chips,
   task shortcuts, and the declaration-kind legend.  The declaration pages use
   the later `body:not(.tl-docs-index)` rules. */
main {
  padding-bottom: 4rem;
}

.tl-docs-index main {
  max-width: 1080px;
  margin-left: auto;
  margin-right: auto;
}

.tl-api-hero {
  margin: 1.25rem 0 1.5rem;
  padding: 1.7rem 1.8rem;
  border: 1px solid rgba(21, 120, 120, 0.18);
  border-radius: 18px;
  background:
    linear-gradient(135deg, color-mix(in srgb, var(--code-bg) 78%, transparent), transparent),
    color-mix(in srgb, var(--body-bg) 88%, var(--code-bg));
  box-shadow: var(--tl-shadow);
}

.tl-api-hero h1 {
  margin: 0.1rem 0 0.55rem;
  font-size: clamp(1.9rem, 3vw, 2.7rem);
  line-height: 1.08;
}

.tl-api-hero p {
  margin: 0;
  max-width: 780px;
}

.tl-hero-actions {
  display: flex;
  flex-wrap: wrap;
  gap: 0.55rem;
  margin-top: 1rem;
}

.tl-hero-actions a {
  display: inline-flex;
  align-items: center;
  padding: 0.5rem 0.72rem;
  border: 1px solid var(--tl-border);
  border-radius: 999px;
  text-decoration: none;
  background: color-mix(in srgb, var(--body-bg) 90%, var(--code-bg));
}

.tl-hero-actions a:first-child {
  background: var(--tl-teal);
  border-color: var(--tl-teal);
  color: white;
}

.tl-kicker {
  color: var(--tl-teal);
  font-weight: 800;
  text-transform: uppercase;
  font-size: 0.78rem;
}

.tl-api-grid {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(240px, 1fr));
  gap: 0.9rem;
  margin: 1rem 0 1.75rem;
}

.tl-api-card {
  display: block;
  min-height: 9rem;
  padding: 1.05rem 1.1rem;
  border: 1px solid var(--tl-border);
  border-radius: 14px;
  background: color-mix(in srgb, var(--body-bg) 88%, var(--code-bg));
  color: var(--text-color);
  text-decoration: none;
  transition: border-color 140ms ease, transform 140ms ease, box-shadow 140ms ease;
}

.tl-api-card:hover {
  border-color: rgba(21, 120, 120, 0.56);
  transform: translateY(-2px);
  box-shadow: var(--tl-shadow);
  text-decoration: none;
}

.tl-api-card span {
  display: block;
  color: var(--tl-teal);
  font-size: 0.78rem;
  font-weight: 800;
  text-transform: uppercase;
}

.tl-api-card strong {
  display: block;
  margin: 0.28rem 0 0.36rem;
  font-family: JuliaMono, monospace;
  font-size: 1.03rem;
  overflow-wrap: anywhere;
}

.tl-api-card p {
  margin: 0;
  color: color-mix(in srgb, var(--text-color) 78%, transparent);
  font-size: 0.94rem;
}

.tl-api-section {
  margin: 1.45rem 0;
}

.tl-api-section h2 {
  color: var(--tl-teal);
  margin-bottom: 0.45rem;
}

.tl-docs-index .tl-api-section:last-of-type {
  margin-bottom: 0;
}

.tl-link-list {
  display: flex;
  flex-wrap: wrap;
  gap: 0.45rem;
}

.tl-link-list a {
  display: inline-block;
  padding: 0.42rem 0.62rem;
  border: 1px solid var(--tl-border);
  border-radius: 999px;
  text-decoration: none;
}

.tl-link-list a:hover {
  border-color: rgba(21, 120, 120, 0.56);
  text-decoration: none;
}

.tl-task-grid {
  display: grid;
  grid-template-columns: minmax(240px, 1.35fr) repeat(2, minmax(210px, 1fr));
  gap: 0.8rem;
  align-items: stretch;
}

.tl-task-grid article,
.tl-task-grid > a {
  border: 1px solid var(--tl-border);
  border-radius: 14px;
  padding: 1rem;
  background: color-mix(in srgb, var(--body-bg) 90%, var(--code-bg));
}

.tl-task-grid article {
  grid-row: span 2;
}

.tl-task-grid article h2 {
  margin-top: 0;
}

.tl-task-grid > a {
  display: block;
  text-decoration: none;
}

.tl-task-grid > a:hover {
  border-color: rgba(21, 120, 120, 0.56);
  box-shadow: var(--tl-shadow);
}

.tl-task-grid strong {
  display: block;
  margin-bottom: 0.25rem;
  color: var(--text-color);
}

.tl-task-grid span {
  display: block;
  color: color-mix(in srgb, var(--text-color) 72%, transparent);
  font-size: 0.95rem;
}

.tl-kind-section {
  padding: 0.95rem 1rem;
  border: 1px solid var(--tl-border);
  border-radius: 14px;
  background: color-mix(in srgb, var(--body-bg) 91%, var(--code-bg));
}

.tl-kind-section p {
  margin: 0.1rem 0 0.75rem;
  color: color-mix(in srgb, var(--text-color) 72%, transparent);
}

.tl-kind-legend {
  display: flex;
  flex-wrap: wrap;
  gap: 0.55rem;
}

.tl-kind-chip {
  display: inline-flex;
  align-items: center;
  gap: 0.4rem;
  padding: 0.38rem 0.6rem;
  border: 1px solid var(--tl-border);
  border-radius: 999px;
  background: color-mix(in srgb, var(--body-bg) 88%, var(--code-bg));
  font-family: JuliaMono, monospace;
  font-size: 0.86rem;
}

.tl-kind-chip::before {
  content: "";
  display: inline-block;
  width: 0.7rem;
  height: 0.7rem;
  border-radius: 999px;
  background: var(--tl-kind-color, var(--text-color));
}

.tl-kind-def {
  --tl-kind-color: var(--def-color);
}

.tl-kind-theorem {
  --tl-kind-color: var(--theorem-color);
}

.tl-kind-structure {
  --tl-kind-color: var(--structure-and-inductive-color);
}

.tl-kind-axiom {
  --tl-kind-color: var(--axiom-and-constant-color);
}

/* Generated declaration pages --------------------------------------------
   DocGen outputs one main module doc block followed by declaration blocks.
   The base HTML is excellent for linking and search, but visually flat.  These
   rules wrap module docs and declarations in subtle cards while preserving the
   colored left/top borders that encode declaration kind. */
body:not(.tl-docs-index) main {
  padding-top: 0.4rem;
}

body:not(.tl-docs-index) .mod_doc {
  margin: 0 0 1.2rem;
  padding: 1rem 1.1rem;
  border: 1px solid var(--tl-border);
  border-radius: 16px;
  background: color-mix(in srgb, var(--body-bg) 91%, var(--code-bg));
  box-shadow: 0 10px 32px rgba(17, 44, 64, 0.05);
}

body:not(.tl-docs-index) .mod_doc h1:first-child,
body:not(.tl-docs-index) main > h1:first-child {
  margin-top: 0;
}

body:not(.tl-docs-index) .decl {
  margin: 1.2rem 0;
}

body:not(.tl-docs-index) .decl > div {
  border-radius: 14px;
  padding: 0.9rem 1rem;
  background: color-mix(in srgb, var(--body-bg) 93%, var(--code-bg));
  box-shadow: 0 10px 28px rgba(17, 44, 64, 0.045);
}

/* Right-side page navigation ---------------------------------------------
   The `.internal_nav` column contains imports, imported-by, and declaration
   anchors for the current page. This polish pass adds cards and hover affordances, plus the
   compact declaration-kind legend on pages with declarations. */
.internal_nav {
  padding: 0.8rem;
  border: 1px solid var(--tl-border);
  border-radius: 14px;
  background: color-mix(in srgb, var(--body-bg) 92%, var(--code-bg));
}

.internal_nav p:first-child {
  margin-top: 0;
}

.internal_nav .imports {
  padding: 0.55rem;
  border: 1px solid rgba(127, 127, 127, 0.16);
  border-radius: 10px;
  background: color-mix(in srgb, var(--body-bg) 88%, var(--code-bg));
}

.internal_nav .nav_link {
  margin: 0.28rem 0;
  padding: 0.24rem 0.35rem 0.24rem 2.35ex;
  border-radius: 8px;
}

.internal_nav .nav_link:hover {
  background: var(--tl-teal-soft);
}

.tl-kind-legend-side {
  margin: 0 0 0.8rem;
  padding: 0.65rem;
  border: 1px solid rgba(127, 127, 127, 0.16);
  border-radius: 10px;
  background: color-mix(in srgb, var(--body-bg) 88%, var(--code-bg));
}

.tl-kind-legend-side strong {
  display: block;
  margin-bottom: 0.35rem;
  color: color-mix(in srgb, var(--text-color) 80%, transparent);
  font-size: 0.84rem;
  text-transform: uppercase;
  letter-spacing: 0.04em;
}

.tl-kind-legend-side .tl-kind-legend {
  gap: 0.35rem;
}

.tl-kind-legend-side .tl-kind-chip {
  padding: 0.22rem 0.42rem;
  font-size: 0.74rem;
}

.tl-kind-legend-side .tl-kind-chip::before {
  width: 0.55rem;
  height: 0.55rem;
}

/* Left module tree --------------------------------------------------------
   The left iframe is generated by DocGen from all imported modules, including
   Lean, Mathlib, and dependencies. A hint and highlight for `NN` show
   users know where the TorchLean modules live. */
.nav {
  padding-right: 0.35rem;
}

.navframe {
  border: 1px solid var(--tl-border);
  border-radius: 14px;
  background: color-mix(in srgb, var(--body-bg) 92%, var(--code-bg));
}

.tl-nav-hint {
  margin: 0.25rem 0 0.65rem;
  padding: 0.55rem 0.65rem;
  border: 1px solid rgba(21, 120, 120, 0.28);
  border-radius: 10px;
  color: color-mix(in srgb, var(--text-color) 82%, transparent);
  background: var(--tl-teal-soft);
  font-size: 0.92rem;
  line-height: 1.35;
}

.tl-nav-hint strong {
  color: var(--text-color);
}

.tl-nav-hint span {
  display: block;
  color: var(--tl-teal);
  font-size: 1.3rem;
  line-height: 1.1;
}

.nav details[data-path="./NN.html"] > summary {
  position: relative;
  padding: 0.2rem 0.25rem;
  border-radius: 8px;
  background: var(--tl-teal-soft);
}

.nav details[data-path="./NN.html"] > summary::after {
  content: "TorchLean";
  margin-left: 0.35rem;
  padding: 0.08rem 0.35rem;
  border-radius: 999px;
  background: var(--tl-teal);
  color: white;
  font-size: 0.72rem;
  font-weight: 700;
}

/* Declaration text and search results ------------------------------------
   Long Lean names and types need breathing room. Monospace stays in place for Lean
   fragments, but slightly increase line height and add understated search
   result separators. */
.nav .nav_file a {
  display: inline-block;
  padding: 0.08rem 0.24rem;
  border-radius: 7px;
}

.nav .nav_file a:hover {
  background: var(--tl-teal-soft);
  text-decoration: none;
}

.decl_header {
  line-height: 1.65;
}

.decl_type,
.structure_field_info,
.constructor {
  line-height: 1.58;
}

pre {
  border: 1px solid rgba(127, 127, 127, 0.16);
  overflow-x: auto;
}

code {
  font-size: 0.92em;
}

body:not(.tl-docs-index) main,
body:not(.tl-docs-index) .mod_doc,
body:not(.tl-docs-index) .def,
body:not(.tl-docs-index) .theorem,
body:not(.tl-docs-index) .opaque,
body:not(.tl-docs-index) .axiom,
body:not(.tl-docs-index) .class,
body:not(.tl-docs-index) .structure,
body:not(.tl-docs-index) .inductive,
body:not(.tl-docs-index) .instance {
  min-width: 0;
  max-width: 100%;
  overflow-x: auto;
}

body:not(.tl-docs-index) .mod_doc a,
body:not(.tl-docs-index) .mod_doc code,
body:not(.tl-docs-index) li code,
body:not(.tl-docs-index) p code,
body:not(.tl-docs-index) :not(pre) > code {
  overflow-wrap: anywhere;
  word-break: break-word;
  white-space: normal !important;
}

#kinds {
  margin: 0.8rem 0 1rem;
  padding: 0.75rem;
  border: 1px solid var(--tl-border);
  border-radius: 12px;
  background: color-mix(in srgb, var(--body-bg) 90%, var(--code-bg));
}

#search_results .result_link,
#search_results .result_doc {
  border-bottom: 1px solid rgba(127, 127, 127, 0.22);
  padding: 0.45rem 0.35rem;
}

/* Mobile cleanup ----------------------------------------------------------
   Small screens cannot support both the site nav and the DocGen drawer.  The
   drawer stays available through the Modules button; secondary site links and
   the right-sidebar declaration legend collapse away. */
@media (max-width: 700px) {
  .tl-docs-index {
    --content-width: calc(100vw - 1.25rem);
  }

  .tl-docs-index header {
    gap: 0.5rem;
  }

  .tl-docs-index header h1 span {
    display: none;
  }

  .tl-docs-index #search_form {
    flex: 1 1 100%;
    margin-left: 0;
  }

  .tl-docsite-links {
    display: none;
  }

  .tl-api-hero {
    padding: 1rem;
  }

  .tl-api-grid,
  .tl-task-grid {
    grid-template-columns: 1fr;
  }

  .tl-task-grid article {
    grid-row: auto;
  }

  .tl-kind-legend-side {
    display: none;
  }
}