1<!DOCTYPE html> 2<html lang="en"> 3 <head> 4 <meta charset="UTF-8"> 5 <base href="../.././"><style>:root { 6 /** Typography **/ 7 /* The font family used for headers, ToC entries, etc */ 8 --verso-structure-font-family: "Helvetica Neue", "Segoe UI", "Roboto", Arial, sans-serif; 9 /* The font family used for body text */ 10 --verso-text-font-family: "Helvetica Neue", "Segoe UI", "Roboto", Arial, sans-serif; 11 /* The font family used for code */ 12 --verso-code-font-family: monospace; 13 14 /** Text colors **/ 15 --verso-text-color: black; 16 --verso-code-color: black; 17 --verso-structure-color: black; 18 19 /** Selected items (e.g. search results) */ 20 --verso-selected-color: #def; 21 22 /** Tooltips **/ 23 /* 24 These colors are used for the tooltips that display documentation and messages for code, 25 and for the equivalent popups that are shown when scripts are unavailable. The 26 severity-specific tooltip colors below default to the foreground and background given 27 here. The separator color draws the rule between sections of a tooltip's content. 28 */ 29 --verso-tooltip-color: black; 30 --verso-tooltip-bg-color: #e5e5e5; 31 --verso-tooltip-border-color: black; 32 --verso-tooltip-separator-color: #ccc; 33 34 /** Message colors **/ 35 /* 36 These colors are used to render Lean's feedback. Each severity (info, warning, error) 37 has four sets of related styles: 38 39 - The affected code itself: foreground and background, both at rest and while hovered, 40 plus the indicator color, which draws the wavy underline marking that a message is 41 present. 42 - The text of the message, via the message color. 43 - The tooltip that displays the message: foreground, background, and border. The border 44 color also draws the accent bar next to a message when it is shown without scripts, 45 and the background also colors the tooltip's arrow. 46 - The marker bar in the margin of output blocks, via the output color. 47 */ 48 --verso-code-info-color: currentcolor; 49 --verso-code-info-bg-color: transparent; 50 --verso-code-info-hover-color: currentcolor; 51 --verso-code-info-hover-bg-color: #4777ff; 52 --verso-info-indicator-color: #4777ff; 53 --verso-message-info-color: black; 54 --verso-tooltip-info-color: var(--verso-tooltip-color); 55 --verso-tooltip-info-bg-color: var(--verso-tooltip-bg-color); 56 --verso-tooltip-info-border-color: #4777ff; 57 --verso-output-info-color: var(--verso-info-indicator-color); 58 59 --verso-code-warning-color: currentcolor; 60 --verso-code-warning-bg-color: transparent; 61 --verso-code-warning-hover-color: currentcolor; 62 --verso-code-warning-hover-bg-color: #ffd580; 63 --verso-warning-indicator-color: #e7a71d; /* 2.11 contrast ratio for white, 9.94 for black */ 64 --verso-message-warning-color: black; 65 --verso-tooltip-warning-color: var(--verso-tooltip-color); 66 --verso-tooltip-warning-bg-color: var(--verso-tooltip-bg-color); 67 --verso-tooltip-warning-border-color: #ffd580; 68 --verso-output-warning-color: var(--verso-warning-indicator-color); 69 70 --verso-code-error-color: currentcolor; 71 --verso-code-error-bg-color: transparent; 72 --verso-code-error-hover-color: currentcolor; 73 --verso-code-error-hover-bg-color: #ffb3b3; 74 --verso-error-indicator-color: #ff0000; 75 --verso-message-error-color: #cc0000; 76 --verso-tooltip-error-color: var(--verso-tooltip-color); 77 --verso-tooltip-error-bg-color: var(--verso-tooltip-bg-color); 78 --verso-tooltip-error-border-color: #ffb3b3; 79 --verso-output-error-color: var(--verso-error-indicator-color); 80 81 /** Proof states **/ 82 /* 83 These colors are used for the proof state displays that can be expanded inside of proofs 84 and shown in tooltips. The toggle colors are used for the control that expands and 85 collapses a proof state. 86 */ 87 --verso-tactic-state-color: black; 88 --verso-tactic-state-bg-color: white; 89 --verso-tactic-state-border-color: #888888; 90 --verso-tactic-toggle-color: #bbbbbb; 91 --verso-tactic-toggle-checked-color: #999999; 92 93 /** Code Highlighting **/ 94 /* 95 These variables control the rendering of Lean code emitted by Verso. Each category that can be 96 highlighted supports the customization of color, weight, style, and family. 97 */ 98 /* Constants (e.g. `List` or `id` or `none`) */
99 --verso-code-const-color: var(--verso-code-color); 100 --verso-code-const-weight: normal; 101 --verso-code-const-style: normal; 102 --verso-code-const-font-family: var(--verso-code-font-family); 103 104 /* Keywords/atoms (e.g. `for` or `def` or `induction`) */ 105 --verso-code-keyword-color: var(--verso-code-color); 106 --verso-code-keyword-weight: bold; 107 --verso-code-keyword-style: normal; 108 --verso-code-keyword-font-family: var(--verso-code-font-family); 109 110 /* Local bindings (e.g. `x` in `let x := 5`) */ 111 --verso-code-var-color: var(--verso-code-color); 112 --verso-code-var-weight: normal; 113 --verso-code-var-style: italic; 114 --verso-code-var-font-family: var(--verso-code-font-family); 115 116 /* The background of interactive code while hovered (hoverable tokens, occurrences of a 117 hovered binding, and the tactics that expand to a proof state) */ 118 --verso-code-hover-bg-color: #eeeeee; 119} 120</style><style> 121 122 123.hl.lean { 124 white-space: pre; 125 font-weight: normal; 126 font-style: normal; 127 font-size: inherit; 128} 129 130.hl.lean .keyword { 131 color: var(--verso-code-keyword-color,); 132 font-weight: var(--verso-code-keyword-weight, bold); 133 font-style: var(--verso-code-keyword-style, normal); 134 font-family: var(--verso-code-keyword-font-family,); 135} 136 137.hl.lean .const { 138 color: var(--verso-code-const-color,); 139 font-weight: var(--verso-code-const-weight, normal); 140 font-style: var(--verso-code-const-style, normal); 141 font-family: var(--verso-code-const-font-family,); 142} 143 144.hl.lean .var { 145 color: var(--verso-code-var-color,); 146 font-weight: var(--verso-code-var-weight, normal); 147 font-style: var(--verso-code-var-style, italic); 148 font-family: var(--verso-code-var-font-family,); 149 150 position: relative; 151} 152 153.hl.lean .literal, .hl.lean .unknown { 154 color: var(--verso-code-color,); 155 font-weight: normal; 156 font-style: normal; 157 font-family: var(--verso-code-font-family,); 158} 159 160/* These lexically-classified token kinds default to the `.unknown` appearance. The rule follows 161 `.const` so it wins for the `anon-ctor` tokens, which also carry the `const` class. */ 162.hl.lean .anon-ctor, 163.hl.lean .number, 164.hl.lean .char, 165.hl.lean .comment, 166.hl.lean .punctuation, 167.hl.lean .delim, 168.hl.lean .wildcard { 169 color: var(--verso-code-color,); 170 font-weight: normal; 171 font-style: normal; 172 font-family: var(--verso-code-font-family,); 173} 174 175.hover-container { 176 width: 0; 177 height: 0; 178 position: relative; 179 display: inline; 180} 181 182.hl.lean a { 183 color: inherit; 184 text-decoration: currentcolor underline dotted; 185} 186 187.hl.lean a:hover { 188 text-decoration: currentcolor underline solid; 189} 190 191/* Links inside tooltips show their underline only when hovered. */ 192.tippy-box .hl.lean a { 193 text-decoration: none; 194} 195 196.hl.lean .hover-info { 197 white-space: normal; 198} 199 200.hl.lean .token .hover-info { 201 display: none; 202 position: absolute; 203 color: var(--verso-tooltip-color, black); 204 background-color: var(--verso-tooltip-bg-color, #e5e5e5); 205 border: 1px solid var(--verso-tooltip-border-color, black); 206 padding: 0.5rem; 207 z-index: 300; 208} 209 210.hl.lean .hover-info.messages { 211 max-height: 10rem; 212 overflow-y: auto; 213 overflow-x: hidden; 214 scrollbar-gutter: stable; 215 padding: 0 0.5rem 0 0; 216 display: block; 217} 218 219.hl.lean .hover-info code { 220 white-space: pre-wrap; 221 background: none; 222} 223 224.hl.lean .hover-info code:not(.verso-message) { 225 color: var(--verso-tooltip-color, black); 226} 227 228.hl.lean .hover-info.messages > code { 229 padding: 0.5rem; 230 display: block; 231 width: fit-content; 232} 233 234.hl.lean .hover-info.messages > code:only-child { 235 margin: 0; 236} 237 238.hl.lean .hover-info.messages > code { 239 margin: 0.1rem; 240} 241 242.hl.lean .hover-info.messages > code:not(:first-child) { 243 margin-top: 0rem; 244} 245 246.hl.lean { 247} 248 249.hl.lean.block { 250 display: block; 251} 252 253.hl.lean.inline { 254 display: inline; 255 white-space: pre-wrap; 256} 257 258.hl.lean * { 259} 260 261.hl.lean .token { 262 transition: all 0.25s; /* Slight fade for highlights */ 263} 264 265@media (hover: hover) { 266 /* Hovered content nested in a collapsed tactic region keeps its plain background: the 267 region's proof state is the tooltip that appears there, and its label is what 268 highlights. `:where` keeps the exclusion out of the specificity computation. */ 269 .hl.lean .token.binding-hl, 270 .hl.lean :is(.literal, .token.typed, .token[data-verso-hover]):hover:not(:where(.tactic:has(> .tactic-toggle:not(:checked)) > label *)) {
271 background-color: var(--verso-code-hover-bg-color, #eeeeee); 272 border-radius: 2px; 273 transition: none; 274 } 275 276 /* Within a hovered message span, token hover backgrounds are removed so the span's own 277 hover background shows across the whole span. The exception is a hovered documented 278 token, which keeps its background because its tooltip is the one shown. */ 279 .hl.lean .has-info:hover .token.binding-hl:not(:hover), 280 .hl.lean .has-info:hover .token.binding-hl:not([data-verso-hover]), 281 .hl.lean .has-info:hover .literal:hover:not([data-verso-hover]), 282 .hl.lean .has-info:hover .token.typed:hover:not([data-verso-hover]) { 283 background-color: transparent; 284 } 285} 286 287 288.hl.lean .has-info .token:not(.tactic-state):not(.tactic-state *), .hl.lean .has-info .inter-text:not(.tactic-state):not(.tactic-state *) { 289 text-decoration-style: wavy; 290 text-decoration-line: underline; 291 text-decoration-thickness: from-font; 292 text-decoration-skip-ink: none; 293} 294 295/* 296The underline color comes from the nearest enclosing message span: each severity's span rule 297sets `--verso--region-indicator-color`, which inherits, so a region nested inside one of 298another severity keeps its own indicator color. 299*/ 300.hl.lean .has-info :not(.tactic-state):not(.tactic-state *) { 301 text-decoration-color: var(--verso--region-indicator-color); 302} 303 304.hl.lean .has-info .hover-info { 305 display: none; 306 position: absolute; 307 transform: translate(0.25rem, 0.3rem); 308 color: var(--verso-tooltip-color, black); 309 border: 1px solid var(--verso-tooltip-border-color, black); 310 padding: 0.5rem; 311 z-index: 400; 312 text-align: left; 313} 314 315.hl.lean .has-info.error { 316 --verso--region-indicator-color: var(--verso-error-indicator-color, #ff0000); 317 --verso--region-hover-color: var(--verso-code-error-hover-color, currentcolor); 318 --verso--region-hover-bg-color: var(--verso-code-error-hover-bg-color, #ffb3b3); 319 color: var(--verso-code-error-color, currentcolor); 320 background-color: var(--verso-code-error-bg-color, transparent); 321} 322 323/* 324The hover highlight follows the tooltip: a message span highlights only when its own tooltip 325is the one that appears. When a hovered nested message span, a hovered documented token, or 326a hovered collapsed tactic label shows its own tooltip instead, the message span does not 327highlight. A span nested in a collapsed tactic region likewise stays plain, because hovering 328it shows the region's proof state; `:where` keeps that exclusion out of the specificity 329computation. 330 331The hover colors come from `--verso--region-hover-color` and `--verso--region-hover-bg-color`, 332which each severity's span rule sets. This keeps the hover conditions in this one rule, and 333because the properties inherit, a region nested inside one of another severity keeps its own 334hover colors. 335*/ 336@media (hover: hover) { 337 .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 *)) { 338 color: var(--verso--region-hover-color, currentcolor); 339 background-color: var(--verso--region-hover-bg-color, transparent); 340 } 341} 342 343.hl.lean .hover-info.messages > code.error { 344 background-color: var(--verso-tooltip-error-bg-color, #e5e5e5); 345 border-left: 0.2rem solid var(--verso-tooltip-error-border-color, #ffb3b3); 346} 347 348/* 349A tooltip that shows only messages of the box's own severity leaves severity styling to the 350box itself. When messages of several severities share the tooltip, or a `mixed` tooltip 351combines messages with other content (such as documentation), each message keeps its 352severity accent to distinguish them. 353*/ 354.tippy-box .hl.lean.mixed > .hover-info.messages { 355 margin-bottom: 0.5rem; 356} 357 358.tippy-box[data-theme~='error'] .hl.lean:not(.mixed) .hover-info.messages:not(:has(> code.warning)):not(:has(> code.information)) > code.error { 359 background: none; 360 border: none; 361} 362 363.error .verso-message, .error .verso-message .token, .error .verso-message label { 364 color: var(--verso-message-error-color, #cc0000); 365} 366 367.error .verso-message .case-label:has(input[type="checkbox"])::before { 368 background-color: var(--verso-message-error-color, #cc0000) !important; 369} 370 371.hl.lean .has-info.warning { 372 --verso--region-indicator-color: var(--verso-warning-indicator-color, #e7a71d);
373 --verso--region-hover-color: var(--verso-code-warning-hover-color, currentcolor); 374 --verso--region-hover-bg-color: var(--verso-code-warning-hover-bg-color, #ffd580); 375 color: var(--verso-code-warning-color, currentcolor); 376 background-color: var(--verso-code-warning-bg-color, transparent); 377} 378 379.hl.lean .hover-info.messages > code.warning { 380 background-color: var(--verso-tooltip-warning-bg-color, #e5e5e5); 381 border-left: 0.2rem solid var(--verso-tooltip-warning-border-color, #ffd580); 382} 383 384.lean-output { 385 border-left: 0.2em solid transparent; 386 padding: 0 0 0 0.5em; 387 border-top-left-radius: 0; 388 border-bottom-left-radius: 0; 389} 390 391.lean-output.error { 392 border-color: var(--verso-output-error-color, var(--verso-error-indicator-color, #ff0000)); 393} 394 395.lean-output.information { 396 border-color: var(--verso-output-info-color, var(--verso-info-indicator-color, #4777ff)); 397} 398 399.lean-output.warning { 400 border-color: var(--verso-output-warning-color, var(--verso-warning-indicator-color, #e7a71d)); 401} 402 403.tippy-box[data-theme~='warning'] .hl.lean:not(.mixed) .hover-info.messages:not(:has(> code.error)):not(:has(> code.information)) > code.warning { 404 background: none; 405 border: none; 406} 407
408.warning .verso-message, .warning .verso-message .token, .warning .verso-message label { 409 color: var(--verso-message-warning-color, black); 410} 411 412.warning .verso-message .case-label:has(input[type="checkbox"])::before { 413 background-color: var(--verso-message-warning-color, black) !important; 414} 415 416 417.hl.lean .has-info.information { 418 --verso--region-indicator-color: var(--verso-info-indicator-color, #4777ff); 419 --verso--region-hover-color: var(--verso-code-info-hover-color, currentcolor); 420 --verso--region-hover-bg-color: var(--verso-code-info-hover-bg-color, #4777ff); 421 color: var(--verso-code-info-color, currentcolor); 422 background-color: var(--verso-code-info-bg-color, transparent); 423} 424 425 426.hl.lean .hover-info.messages > code.information { 427 background-color: var(--verso-tooltip-info-bg-color, #e5e5e5); 428 border-left: 0.2rem solid var(--verso-tooltip-info-border-color, #4777ff); 429} 430 431.tippy-box[data-theme~='info'] .hl.lean:not(.mixed) .hover-info.messages:not(:has(> code.error)):not(:has(> code.warning)) > code.information { 432 background: none; 433 border: none; 434} 435 436.information .verso-message, .information .verso-message .token, .information .verso-message label { 437 color: var(--verso-message-info-color, black); 438} 439 440.information .verso-message .case-label:has(input[type="checkbox"])::before { 441 background-color: var(--verso-message-info-color, black) !important; 442} 443 444.hl.lean div.docstring { 445 font-family: var(--verso-text-font-family, sans-serif); 446 white-space: normal; 447 max-width: calc(min(40rem, 90vw)); 448 width: max-content; 449} 450 451.hl.lean div.docstring > :last-child { 452 margin-bottom: 0; 453} 454 455.hl.lean div.docstring > :first-child { 456 margin-top: 0; 457} 458 459.hl.lean .hover-info .sep { 460 display: block; 461 width: auto; 462 margin-left: 1rem; 463 margin-right: 1rem; 464 margin-top: 0.5rem; 465 margin-bottom: 0.5rem; 466 padding: 0; 467 height: 1px; 468 border-top: 1px solid var(--verso-tooltip-separator-color, #ccc); 469} 470 471.hl.lean code { 472 font-family: var(--verso-code-font-family); 473} 474 475.hl.lean .tactic-state { 476 display: none; 477 position: relative; 478 width: fit-content; 479 border: 1px solid var(--verso-tactic-state-border-color, #888888); 480 border-radius: 0.1rem; 481 padding: 0.5rem; 482 font-family: sans-serif; 483 color: var(--verso-tactic-state-color, black); 484 background-color: var(--verso-tactic-state-bg-color, white); 485} 486 487.hl.lean.popup .tactic-state { 488 position: static; 489 display: block; 490 width: auto; 491 border: none; 492 padding: 0.5rem; 493 font-family: sans-serif; 494 background-color: var(--verso-tactic-state-bg-color, white); 495} 496 497 498.hl.lean .tactic { 499 position: relative; 500 display: inline; 501 vertical-align: top; 502 /* Without these, mobile Safari will start making font sizes inconsistent when its text size adjustment feature is triggered.*/ 503 -webkit-text-size-adjust: 100%; 504 text-size-adjust: 100%; 505} 506 507.hl.lean .tactic:has(> .tactic-toggle:checked) { 508 display: inline-grid; 509 grid-template-columns: 1fr; 510} 511 512.hl.lean .tactic-toggle:checked ~ .tactic-state { 513 display: inline-block; 514 vertical-align: top; 515 grid-row: 2; 516 justify-self: start; 517} 518 519.hl.lean .tactic > label { 520 position: relative; 521 grid-row: 1; 522 display: inline; 523} 524 525@media (hover: hover) { 526 /* Highlight a region on hover only when its own toggle is unchecked, and only the innermost 527 hovered region: `label:hover` bubbles to ancestor labels, so suppress the highlight on a region 528 whose label contains a more deeply nested hovered tactic label. The region's proof state is the 529 tooltip for everything else in its label, so the label keeps its highlight while any of that 530 content is hovered. */ 531 .hl.lean .tactic:has(> .tactic-toggle:not(:checked)) > label:hover:not(:has(.tactic > label:hover)) { 532 background-color: var(--verso-code-hover-bg-color, #eeeeee); 533 } 534} 535 536.hl.lean .tactic-toggle { 537 position: absolute; 538 top: 0; 539 left: 0; 540 opacity: 0; 541 height: 0; 542 width: 0; 543 z-index: -10; 544} 545 546.hl.lean .tactic > label::after { 547 content: ""; 548 border: 1px solid var(--verso-tactic-toggle-color, #bbbbbb); 549 /* These need to be em, not rem, to scale with the font */ 550 border-radius: 1em; 551 height: 0.25em; 552 vertical-align: middle; 553 width: 0.6em; 554 margin-left: 0.1em; 555 margin-right: 0.1em; 556 display: inline-block; 557 transition: all 0.5s; 558} 559 560/* 561@media (hover: hover) { 562 .hl.lean .tactic > label:hover::after { 563 border: 1px solid #aaaaaa; 564 background-color: #aaaaaa; 565 transition: all 0.5s; 566 } 567} 568*/ 569 570.hl.lean .tactic > label:has(+ .tactic-toggle:checked)::after { 571 border: 1px solid var(--verso-tactic-toggle-checked-color, #999999); 572 background-color: var(--verso-tactic-toggle-checked-color, #999999); 573 transition: all 0.5s; 574} 575 576.hl.lean .tactic-state .goal + .goal { 577 margin-top: 1.5em; 578} 579
580/* 581Some CSS frameworks customize details/summary in ways not compatible with Verso's output. 582*/ 583 584.hl.lean details { 585 display: block !important; 586 margin: 0; 587} 588 589.hl.lean details summary { 590 display: list-item !important; 591 margin: 0; 592} 593 594.hl.lean details summary:focus { 595 outline: none; 596 outline-offset: none; 597 color: inherit; 598} 599 600.hl.lean ul > li { 601 margin-bottom: 0; 602} 603 604.hl.lean details summary::marker { 605 display: inline !important; 606} 607 608.hl.lean details > summary:first-of-type { 609 list-style-type: disclosure-closed; 610 list-style-position: inside; 611} 612 613.hl.lean details[open] > summary:first-of-type { 614 list-style-type: disclosure-open; 615} 616 617.hl.lean details summary::before, .hl.lean details summary::after { 618 content: "" !important; 619 background: none; 620 display: none; 621} 622 623.hl.lean .tactic-state summary { 624 /* These need to be em, not rem, to scale with the font */ 625 margin-left: -0.5em; 626} 627 628.hl.lean .tactic-state details { 629 /* These need to be em, not rem, to scale with the font */ 630 padding-left: 0.5em; 631} 632 633.hl.lean .case-label { 634 display: block; 635 position: relative; 636} 637 638.hl.lean .case-label input[type="checkbox"] { 639 position: absolute; 640 top: 0; 641 left: 0; 642 opacity: 0; 643 height: 0; 644 width: 0; 645 z-index: -10; 646} 647 648.hl.lean .case-label:has(input[type="checkbox"])::before { 649 display: inline-block; 650 background-color: currentcolor; 651 content: ' '; 652 transition: ease 0.2s; 653 margin-right: 0.7em; 654 clip-path: polygon(100% 0, 0 0, 50% 100%); 655 width: 0.6em; 656 height: 0.6em; 657 vertical-align: middle; 658} 659 660.hl.lean .case-label:has(input[type="checkbox"]:not(:checked))::before { 661 transform: rotate(-90deg); 662} 663 664.hl.lean .case-label:has(input[type="checkbox"]) { 665 666} 667 668.hl.lean .case-label:has(input[type="checkbox"]:checked) { 669 670} 671 672 673.hl.lean .labeled-case > :not(:first-child) { 674 max-height: 0px; 675 display: block; 676 overflow: hidden; 677 transition: max-height 0.1s ease-in; 678 /* These need to be em, not rem, to scale with the font */ 679 margin-left: 0.5em; 680 margin-top: 0.1em; 681} 682 683.hl.lean .labeled-case:has(.case-label input[type="checkbox"]:checked) > :not(:first-child) { 684 max-height: 100%; 685} 686 687 688.hl.lean .goal-name::before { 689 font-style: normal; 690 content: "case "; 691} 692 693.hl.lean .goal-name { 694 font-style: italic; 695 font-family: var(--verso-code-font-family); 696 color: inherit; 697} 698 699.hl.lean .hypotheses { 700 display: table; 701} 702 703.hl.lean .hypothesis { 704 display: table-row; 705} 706 707.hl.lean .hypothesis > * { 708 display: table-cell; 709} 710 711 712.hl.lean .hypotheses .colon { 713 text-align: center; 714 /* This needs to be em, not rem, to scale with the font */ 715 min-width: 1em; 716} 717 718.hl.lean .hypotheses .name { 719 text-align: right; 720} 721 722.hl.lean .hypotheses .name, 723.hl.lean .hypotheses .type, 724.hl.lean .conclusion .type { 725 font-family: var(--verso-code-font-family); 726} 727 728.tippy-box { 729 /* Without these, mobile Safari will start making font sizes inconsistent when its text size adjustment feature is triggered.*/ 730 -webkit-text-size-adjust: 100%; 731 text-size-adjust: 100%; 732} 733 734/* 735Tippy's stylesheet paints each arrow's fill triangle with the arrow element's `color` (its 736placement-specific `::before` rules use `border-color: initial`, which is `currentcolor`), 737and its border extension paints the outline triangle with the box's border color. Setting 738`color` on the arrow therefore matches it to the tooltip background for every placement. 739*/ 740.tippy-box[data-theme~='lean'] { 741 background-color: var(--verso-tooltip-bg-color, #e5e5e5); 742 color: var(--verso-tooltip-color, black); 743 border: 1px solid var(--verso-tooltip-border-color, black); 744} 745.tippy-box[data-theme~='lean'] > .tippy-arrow { 746 color: var(--verso-tooltip-bg-color, #e5e5e5); 747} 748 749.tippy-box[data-theme~='message'][data-placement^='top'] > .tippy-arrow::before { 750 border-width: 11px 11px 0; 751} 752.tippy-box[data-theme~='message'][data-placement^='top'] > .tippy-arrow::after { 753 bottom: -11px; 754 border-width: 11px 11px 0; 755} 756.tippy-box[data-theme~='message'][data-placement^='bottom'] > .tippy-arrow::before { 757 border-width: 0 11px 11px; 758} 759.tippy-box[data-theme~='message'][data-placement^='bottom'] > .tippy-arrow::after { 760 top: -11px; 761 border-width: 0 11px 11px; 762} 763.tippy-box[data-theme~='message'][data-placement^='left'] > .tippy-arrow::before { 764 border-width: 11px 0 11px 11px; 765} 766.tippy-box[data-theme~='message'][data-placement^='left'] > .tippy-arrow::after { 767 right: -11px; 768 border-width: 11px 0 11px 11px; 769} 770 771.tippy-box[data-theme~='message'][data-placement^='right'] > .tippy-arrow::before { 772 border-width: 11px 11px 11px 0; 773} 774.tippy-box[data-theme~='message'][data-placement^='right'] > .tippy-arrow::after { 775 left: -11px; 776 border-width: 11px 11px 11px 0; 777} 778 779 780 781.tippy-box[data-theme~='warning'] { 782 background-color: var(--verso-tooltip-warning-bg-color, #e5e5e5); 783 color: var(--verso-tooltip-warning-color, black); 784 border: 3px solid var(--verso-tooltip-warning-border-color, #ffd580); 785} 786.tippy-box[data-theme~='warning'] > .tippy-arrow { 787 color: var(--verso-tooltip-warning-bg-color, #e5e5e5); 788} 789 790.tippy-box[data-theme~='error'] { 791 background-color: var(--verso-tooltip-error-bg-color, #e5e5e5); 792 color: var(--verso-tooltip-error-color, black); 793 border: 3px solid var(--verso-tooltip-error-border-color, #ffb3b3); 794} 795.tippy-box[data-theme~='error'] > .tippy-arrow { 796 color: var(--verso-tooltip-error-bg-color, #e5e5e5); 797} 798 799.tippy-box[data-theme~='info'] { 800 background-color: var(--verso-tooltip-info-bg-color, #e5e5e5); 801 color: var(--verso-tooltip-info-color, black); 802 border: 3px solid var(--verso-tooltip-info-border-color, #4777ff); 803} 804.tippy-box[data-theme~='info'] > .tippy-arrow { 805 color: var(--verso-tooltip-info-bg-color, #e5e5e5); 806} 807 808.tippy-box[data-theme~='tactic'] { 809 background-color: var(--verso-tactic-state-bg-color, white); 810 color: var(--verso-tactic-state-color, black); 811 border: 1px solid var(--verso-tactic-state-border-color, #888888); 812} 813.tippy-box[data-theme~='tactic'] > .tippy-arrow { 814 color: var(--verso-tactic-state-bg-color, white); 815} 816 817.extra-doc-links { 818 list-style-type: none; 819 margin-left: 0; 820 padding: 0; 821} 822 823.extra-doc-links > li { 824 display: inline-block; 825} 826 827.extra-doc-links > li:not(:last-child)::after {
828 content: '|'; 829 display: inline-block; 830 margin: 0 0.25em; 831} 832 833.verso-message .trace { 834 display: block; 835} 836 837.verso-message .trace > summary::marker { 838 color: var(--verso-text-color, black); 839} 840 841.verso-message .trace-children { 842 margin: 0; 843 padding: 0; 844} 845 846.verso-message .trace-children > li { 847 list-style-type: none; 848 margin-left: 1.5em; 849} 850 851.verso-message .trace-children > li:not(:has(.trace)) { 852 margin-left: 0; 853} 854 855.verso-message .trace-class { 856 color: color-mix(in srgb, currentColor 70%, transparent); 857 font-weight: bold; 858 margin: 0; 859 padding: 0; 860} 861 862.verso-message .text { 863 white-space: pre-wrap; 864} 865 866 867</style>
868<script> 869 870 871window.onload = async () => { 872 873 // Don't show hovers inside of closed tactic states 874 function blockedByTactic(elem) { 875 let parent = elem.parentNode; 876 while (parent && "classList" in parent) { 877 if (parent.classList.contains("tactic")) { 878 const toggle = parent.querySelector(":scope > input.tactic-toggle"); 879 if (toggle) { 880 return !toggle.checked; 881 } 882 } 883 parent = parent.parentNode; 884 } 885 return false; 886 } 887 888 // The innermost element under the pointer, used to show only the most specific hover 889 let hoverTarget = null; 890 document.addEventListener('mouseover', (e) => { hoverTarget = e.target; }, true); 891 892 // Visible tippy references; a tooltip is blocked while an unrelated one is visible 893 const visibleTippies = new Set(); 894 function blockedByTippy(elem) { 895 for (const ref of visibleTippies) { 896 if (!ref.contains(elem) && !elem.contains(ref)) return true; 897 } 898 return false; 899 } 900 901 // Whether the element's tooltip would have content to show. Content nested in a 902 // collapsed tactic region is covered by the region's proof-state tooltip, whether or 903 // not a tippy instance is currently attached to it. 904 function showsContent(el) { 905 if (!el._tippy) return false; 906 if (el.classList.contains('tactic')) { 907 const toggle = el.querySelector(':scope > input.tactic-toggle'); 908 return !!toggle && !toggle.checked; 909 } 910 return (!!el.querySelector('.hover-info') || 'versoHover' in el.dataset) && 911 !blockedByTactic(el); 912 } 913 914 // The nearest enclosing element whose tooltip has content 915 function innermostShowable(el) { 916 while (el && el.nodeType === Node.ELEMENT_NODE) { 917 if (showsContent(el)) return el; 918 el = el.parentElement; 919 } 920 return null; 921 } 922 923 // Binding highlights via event delegation with cached lookups 924 const bindingCache = new Map(); // context+binding -> [token elements] 925 let highlightedTokens = []; 926 function getBindingTokens(context, binding) { 927 const key = context + "\0" + binding; 928 let tokens = bindingCache.get(key); 929 if (!tokens) { 930 tokens = []; 931 for (const example of document.querySelectorAll(".hl.lean")) { 932 if (example.dataset.leanContext == context) { 933 for (const tok of example.querySelectorAll(".token[data-binding=\"" + CSS.escape(binding) + "\"]")) { 934 tokens.push(tok); 935 } 936 } 937 } 938 bindingCache.set(key, tokens); 939 } 940 return tokens; 941 } 942 for (const container of document.querySelectorAll(".hl.lean")) { 943 container.addEventListener("mouseover", (event) => { 944 const c = event.target.closest(".token"); 945 if (!c || !c.dataset.binding || c.dataset.binding === "" || !container.contains(c)) return; 946 if (blockedByTactic(c)) return; 947 const tokens = getBindingTokens(container.dataset.leanContext, c.dataset.binding); 948 for (const tok of tokens) { 949 tok.classList.add("binding-hl"); 950 } 951 highlightedTokens = tokens; 952 }); 953 container.addEventListener("mouseout", (event) => { 954 const c = event.target.closest(".token"); 955 if (!c || !container.contains(c)) return; 956 for (const tok of highlightedTokens) { 957 tok.classList.remove("binding-hl"); 958 } 959 highlightedTokens = []; 960 }); 961 } 962 /* Render docstrings */ 963 if ('undefined' !== typeof marked) { 964 for (const d of document.querySelectorAll("code.docstring, pre.docstring")) { 965 const str = d.innerText; 966 const html = marked.parse(str); 967 const rendered = document.createElement("div"); 968 rendered.classList.add("docstring"); 969 rendered.innerHTML = html; 970 d.parentNode.replaceChild(rendered, d); 971 } 972 } 973 // Add hovers 974 const versoDocData = await (fetch("-verso-docs.json").then((resp) => resp.json())); 975 976 function hideParentTooltips(element) { 977 let parent = element.parentElement; 978 while (parent) { 979 const tippyInstance = parent._tippy; 980 if (tippyInstance) { 981 tippyInstance.hide(); 982 } 983 parent = parent.parentElement; 984 } 985 } 986 987 function hideDescendantTooltips(element) { 988 for (const ref of visibleTippies) { 989 if (ref !== element && element.contains(ref)) { 990 ref._tippy.hide(); 991 } 992 } 993 } 994 995 // Renders the documentation for a hover ID from the doc table 996 function docHoverContent(hoverId) { 997 const info = document.createElement('span'); 998 info.className = 'hover-info'; 999 info.style.display = 'block'; 1000 const data = versoDocData[hoverId]; 1001 if (data) { 1002 info.innerHTML = data; 1003 /* Render docstrings - TODO server-side */ 1004 if ('undefined' !== typeof marked) { 1005 for (const d of info.querySelectorAll('code.docstring, pre.docstring')) { 1006 const str = d.innerText; 1007 const html = marked.parse(str); 1008 const rendered = document.createElement('div'); 1009 rendered.classList.add('docstring'); 1010 rendered.innerHTML = html; 1011 d.parentNode.replaceChild(rendered, d); 1012 } 1013 } 1014 } else { 1015 info.innerHTML = 'Failed to load doc ID: ' + hoverId; 1016 } 1017 return info; 1018 } 1019 1020 1021 1022 1023 const defaultTippyProps = { 1024 /* DEBUG -- remove the space: * / 1025 onHide(any) { return false; }, 1026 trigger: "click", 1027 // */ 1028 /* theme: "lean", */ 1029 maxWidth: "none", 1030 appendTo: () => document.body, 1031 interactive: true, 1032 delay: [100, null], 1033 /* ignoreAttributes: true, */ 1034 followCursor: 'initial', 1035 onShow(inst) { 1036 const ref = inst.reference; 1037 if (ref.className == 'tactic') { 1038 const toggle = ref.querySelector(":scope > input.tactic-toggle"); 1039 if (toggle && toggle.checked) { 1040 return false;
1041 } 1042 } else if (ref.querySelector(".hover-info") || "versoHover" in ref.dataset) { 1043 if (blockedByTactic(ref)) { return false }; 1044 } else { // Nothing to show here! 1045 return false; 1046 } 1047 // Show only the most specific hover under the pointer 1048 if (hoverTarget && ref.contains(hoverTarget) && innermostShowable(hoverTarget) !== ref) { 1049 return false; 1050 } 1051 hideParentTooltips(ref); 1052 hideDescendantTooltips(ref); 1053 if (blockedByTippy(ref)) { return false; } 1054 }, 1055 onShown(inst) { visibleTippies.add(inst.reference); }, 1056 onHidden(inst) { visibleTippies.delete(inst.reference); }, 1057 content (tgt) { 1058 const content = document.createElement("span"); 1059 if (tgt.className == 'tactic') { 1060 const state = tgt.querySelector(":scope > .tactic-state").cloneNode(true); 1061 state.style.display = "block"; 1062 content.appendChild(state); 1063 content.style.display = "block"; 1064 content.className = "hl lean popup"; 1065 } else { 1066 content.className = "hl lean"; 1067 content.style.display = "block"; 1068 content.style.maxHeight = "300px"; 1069 content.style.overflowY = "auto"; 1070 content.style.overflowX = "hidden"; 1071 // Messages come from the inline hover-info; documentation comes from the doc 1072 // table. An element with both (a message span sharing a documented token's 1073 // extent) shows both in one tooltip. 1074 const hoverId = tgt.dataset.versoHover; 1075 const hoverInfo = tgt.querySelector(".hover-info"); 1076 if (hoverInfo) { 1077 content.appendChild(hoverInfo.cloneNode(true)); 1078 } 1079 if (hoverId) { 1080 // TODO stop doing an implicit conversion from string to number here 1081 content.appendChild(docHoverContent(hoverId)); 1082 } 1083 if (hoverInfo && hoverId) { 1084 content.classList.add('mixed'); 1085 } 1086 const extraLinks = tgt.dataset['versoLinks'] || tgt.parentElement.dataset['versoLinks']; 1087 if (extraLinks) { 1088 try { 1089 const extras = JSON.parse(extraLinks); 1090 const links = document.createElement('ul'); 1091 links.className = 'extra-doc-links'; 1092 extras.forEach((l) => { 1093 const li = document.createElement('li'); 1094 li.innerHTML = "<a href=\"" + l['href'] + "\" title=\"" + l.long + "\">" + l.short + "</a>"; 1095 links.appendChild(li); 1096 }); 1097 content.appendChild(links); 1098 } catch (error) { 1099 console.error(error); 1100 } 1101 } 1102 } 1103 return content; 1104 } 1105 }; 1106 1107 1108 document.querySelectorAll('.hl.lean .const.token, .hl.lean .keyword.token, .hl.lean .literal.token, .hl.lean .option.token, .hl.lean .var.token, .hl.lean .typed.token, .hl.lean .level-var, .hl.lean .level-const, .hl.lean .level-op, .hl.lean .sort').forEach(element => { 1109 element.setAttribute('data-tippy-theme', 'lean'); 1110 }); 1111 document.querySelectorAll('.hl.lean .has-info.warning').forEach(element => { 1112 element.setAttribute('data-tippy-theme', 'warning message'); 1113 }); 1114 document.querySelectorAll('.hl.lean .has-info.information').forEach(element => { 1115 element.setAttribute('data-tippy-theme', 'info message'); 1116 }); 1117 document.querySelectorAll('.hl.lean .has-info.error').forEach(element => { 1118 element.setAttribute('data-tippy-theme', 'error message'); 1119 }); 1120 document.querySelectorAll('.hl.lean .tactic').forEach(element => { 1121 element.setAttribute('data-tippy-theme', 'tactic'); 1122 }); 1123 // Skip tokens inside closed tactics â they interfere with tactic tippys 1124 const closedTactics = new Set(); 1125 document.querySelectorAll('.hl.lean .tactic').forEach(tactic => { 1126 const toggle = tactic.querySelector(':scope > input.tactic-toggle'); 1127 if (toggle && !toggle.checked) closedTactics.add(tactic); 1128 }); 1129 function isInsideClosedTactic(el) { 1130 const tactic = el.closest('.tactic'); 1131 return tactic && tactic !== el && closedTactics.has(tactic); 1132 } 1133 1134 const tokenSelector = '.hl.lean .const.token, .hl.lean .keyword.token, .hl.lean .literal.token, .hl.lean .option.token, .hl.lean .var.token, .hl.lean .typed.token, .hl.lean .has-info, .hl.lean .tactic, .hl.lean .level-var, .hl.lean .level-const, .hl.lean .level-op, .hl.lean .sort'; 1135 tippy(Array.from(document.querySelectorAll(tokenSelector)).filter(el => !isInsideClosedTactic(el)), defaultTippyProps); 1136 1137 // Create/destroy token tippys when tactic checkbox toggles 1138 const tacticTippySelector = '.const.token, .keyword.token, .literal.token, .option.token, .var.token, .typed.token, .has-info, .level-var, .level-const, .level-op, .sort'; 1139 document.querySelectorAll('.hl.lean .tactic').forEach(tactic => { 1140 const toggle = tactic.querySelector(':scope > input.tactic-toggle'); 1141 if (toggle) toggle.addEventListener('change', () => { 1142 if (toggle.checked) { 1143 closedTactics.delete(tactic); 1144 tactic.querySelectorAll(tacticTippySelector).forEach(el => { 1145 if (!el._tippy) { 1146 tippy(el, defaultTippyProps); 1147 } 1148 }); 1149 } else { 1150 closedTactics.add(tactic); 1151 tactic.querySelectorAll(tacticTippySelector).forEach(el => { 1152 if (el._tippy) el._tippy.destroy(); 1153 }); 1154 } 1155 // The toggle changes which element's tooltip belongs to the pointer's position, 1156 // but the pointer stays put, so no hover event announces the change. Show the 1157 // right tooltip once the click that flipped the toggle has hidden the old one. 1158 setTimeout(() => { 1159 if (hoverTarget && hoverTarget.isConnected) { 1160 const showable = innermostShowable(hoverTarget); 1161 if (showable && showable._tippy) showable._tippy.show(); 1162 } 1163 }, 0); 1164 }); 1165 }); 1166} 1167 1168</script>
1168 1169
1170<script> 1171 1172document.addEventListener("DOMContentLoaded", () => { 1173 for (const m of document.querySelectorAll(".math.inline")) { 1174 katex.render(m.textContent, m, {throwOnError: false, displayMode: false}); 1175 } 1176 for (const m of document.querySelectorAll(".math.display")) { 1177 katex.render(m.textContent, m, {throwOnError: false, displayMode: true}); 1178 } 1179}); 1180</script>
1180 1181
1182<script src="-verso-data/dark.js"></script>
1182 1183
1183<script src="-verso-data/theme.js"></script>
1183 1184
1184<script src="-verso-data/copy.js"></script>
1184 1185
1185<script src="-verso-data/motion.js"></script>
1185 1186
1186<script src="-verso-data/navbar.js"></script>
1186 1187
1187<script src="-verso-data/popper.js"></script>
1187 1188
1188<script src="-verso-data/tippy.js"></script>
1188 1189
1189<script src="-verso-data/testimonials.js"></script>
1189 1190
1190<script src="-verso-data/glightbox.min.js"></script>
1190 1191
1191<script src="-verso-data/gallery.js"></script>
1191 1192
1192<script src="-verso-data/fro.js"></script>
1192 1193 <link rel="stylesheet" href="-verso-data/reset.css"> 1194 <link rel="stylesheet" href="-verso-data/layout.css"> 1195 <link rel="stylesheet" href="-verso-data/navbar.css"> 1196 <link rel="stylesheet" href="-verso-data/footer.css"> 1197 <link rel="stylesheet" href="-verso-data/theme.css"> 1198 <link rel="stylesheet" href="-verso-data/article.css"> 1199 <link rel="stylesheet" href="-verso-data/card.css"> 1200 <link rel="stylesheet" href="-verso-data/copy-button.css"> 1201 <link rel="stylesheet" href="-verso-data/tippy-border.css"> 1202 <link rel="stylesheet" href="-verso-data/action.css"> 1203 <link rel="stylesheet" href="-verso-data/timeline.css"> 1204 <link rel="stylesheet" href="-verso-data/testimonials.css"> 1205 <link rel="stylesheet" href="-verso-data/steps.css"> 1206 <link rel="stylesheet" href="-verso-data/glightbox.css"> 1207 <link rel="stylesheet" href="-verso-data/gallery.css"> 1208 <link rel="stylesheet" href="-verso-data/zulipInfo.css"> 1209 <link rel="stylesheet" href="-verso-data/org-hero.css"> 1210 <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css" integrity="sha384-n8MVd4RsNIU0tAv4ct0nTaAbDJwPJzDEaqSD1odI+WdtXRGWt2kTvGFasHpSy3SV" crossorigin="anonymous"> 1211
1211<script defer="defer" src="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.js" integrity="sha384-XjKyOOlGwcjNTAIQHIpgOno0Hl1YQqzUOEleOLALmuqehneUG+vnGctmUb0ZY0l8" crossorigin="anonymous"></script>
1211 1212
1212<script src="https://cdn.jsdelivr.net/npm/[email protected]/marked.min.js" integrity="sha384-zbcZAIxlvJtNE3Dp5nxLXdXtXyxwOdnILY1TDPVmKFhl4r4nSUG1r8bcFXGVa4Te" crossorigin="anonymous"></script>
1212 1213 <style> 1214 1215 @media (scripting: none) { 1216 #selector-input---verso-component-5-2:checked ~ .selector-list .selector-button[for="selector-input---verso-component-5-2"] { 1217 background-color: var(--color-primary); 1218 color: white; 1219 } 1220 1221 #--verso-component-5-panel-2 { 1222 display: none; 1223 } 1224 1225 #selector-input---verso-component-5-2:checked ~ .selector-panels > #--verso-component-5-panel-2 { 1226 display: block; 1227 } 1228 } 1229 1230</style> 1231<style> 1232.sponsors-section { 1233 background: var(--color-white); 1234 padding: var(--space-16) 0; 1235} 1236 1237.dark-theme .sponsors-section { 1238 background: #111; 1239} 1240 1241.sponsors { 1242 display: flex; 1243 flex-direction: column; 1244 align-content: center; 1245 align-items: center; 1246} 1247 1248.sponsors-content { 1249 display: grid; 1250 grid-template-columns: repeat(3, 1fr); 1251 max-width: 900px; 1252 width: 100%; 1253} 1254 1255.sponsor { 1256 min-height: 95px; 1257 display: flex; 1258 align-items: center; 1259 justify-content: center; 1260 padding: var(--space-8) var(--space-6); 1261} 1262 1263/* centre a sponsor that ends up alone on the last row */ 1264.sponsor:last-child:nth-child(3n+1):not(:first-child) { 1265 grid-column: 2; 1266} 1267 1268img.sponsor-logo { 1269 width: 100%; 1270 max-width: 250px; 1271 max-height: 90px; 1272 object-fit: contain; 1273 opacity: 0.8; 1274 transition: opacity var(--transition-base); 1275} 1276 1277.sponsor:hover img.sponsor-logo { 1278 opacity: 1; 1279} 1280 1281@media (max-width: 768px) { 1282 .sponsors { 1283 width: calc(100% - var(--space-8)*2); 1284 } 1285 1286 .sponsors-content { 1287 grid-template-columns: repeat(2, 1fr); 1288 width: 100%; 1289 } 1290 1291 /* two columns leave no middle to centre in, so a lone sponsor spans the row */ 1292 .sponsor:last-child:nth-child(odd):not(:first-child) { 1293 grid-column: 1 / -1; 1294 } 1295} 1296 1297.dark-theme .sponsor-logo { 1298 filter: invert(1) brightness(10); 1299} 1300 1301/* Sponsors that ship a dedicated dark logo swap the image instead of inverting it. */ 1302.sponsor-logo-dark { 1303 display: none; 1304} 1305 1306.dark-theme .sponsor-logo-light { 1307 display: none; 1308} 1309 1310.dark-theme .sponsor-logo-dark { 1311 display: block; 1312} 1313 1314.dark-theme .sponsor-logo-light, 1315.dark-theme .sponsor-logo-dark { 1316 filter: none; 1317} 1318 1319</style> 1320<style> 1321.button { 1322 border-radius: var(--radius-md); 1323 padding: var(--space-4) var(--space-12); 1324 display: flex; 1325 align-items: center; 1326 gap: var(--space-3); 1327 justify-content: center; 1328 font-size: var(--fs-md); 1329 font-weight: 500; 1330 cursor: pointer; 1331 transition: all var(--transition-base); 1332} 1333 1334a.primary { 1335 background: var(--color-primary); 1336 color: var(--color-text-contrast); 1337 fill: var(--color-text-contrast); 1338} 1339 1340a.primary svg { 1341 fill: var(--color-text-contrast); 1342} 1343 1344a.primary:hover { 1345 background: var(--color-primary-light) !important; 1346 color: var(--color-text-contrast) !important; 1347 border: 0px !important; 1348} 1349 1350a.primary:focus { 1351 background: var(--color-primary-focus); 1352 color: var(--color-text-contrast); 1353} 1354 1355.secondary { 1356 border: 2px solid var(--color-primary); 1357 background: var(--color-white); 1358 color: var(--color-primary); 1359} 1360 1361.secondary:hover { 1362 background: var(--color-primary); 1363 fill: var(--color-text-contrast); 1364 color: var(--color-text-contrast); 1365} 1366 1367.secondary:hover svg { 1368 fill: var(--color-text-contrast); 1369} 1370 1371.primary.inverted { 1372 background: var(--color-text-contrast); 1373 color: var(--color-primary); 1374 fill: var(--color-primary); 1375} 1376 1377.primary.inverted svg { 1378 fill: var(--color-text-contrast); 1379} 1380 1381.primary.inverted:hover { 1382 background: #e9e9e9; 1383} 1384 1385.primary.inverted:focus { 1386 background: var(--color-primary-focus); 1387 color: var(--color-text-contrast); 1388} 1389 1390.secondary.inverted { 1391 border: 2px solid var(--color-text-contrast); 1392 background: transparent; 1393 color: var(--color-text-contrast); 1394} 1395 1396.secondary.inverted:hover { 1397 background: var(--color-text-contrast); 1398 fill: var(--color-primary); 1399 color: var(--color-primary); 1400} 1401 1402.secondary.inverted:hover svg { 1403 fill: var(--color-white); 1404} 1405</style> 1406<style> 1407 1408 @media (scripting: none) { 1409 #selector-input---verso-component-5-0:checked ~ .selector-list .selector-button[for="selector-input---verso-component-5-0"] { 1410 background-color: var(--color-primary); 1411 color: white; 1412 } 1413 1414 #--verso-component-5-panel-0 { 1415 display: none; 1416 } 1417 1418 #selector-input---verso-component-5-0:checked ~ .selector-panels > #--verso-component-5-panel-0 { 1419 display: block; 1420 } 1421 } 1422 1423</style> 1424<style> 1425.card-grid { 1426 display: grid; 1427 grid-template-columns: repeat(2, 1fr); 1428 gap: 16px; 1429} 1430 1431.card-grid > :last-child:nth-child(odd) { 1432 grid-column: span 2; 1433} 1434 1435.main-learn-card { 1436 display: flex; 1437 flex-direction: column; 1438 transition: background-color var(--transition-base), border-color var(--transition-base); 1439 justify-content: space-between; 1440 padding: 40px; 1441 align-content: center; 1442 gap: 20px; 1443} 1444 1445a.card-href.card.main-learn-card { 1446 position: relative; 1447 background: var(--card-bg); 1448 border: 1px solid var(--color-border) !important; 1449 border-radius: var(--radius-md); 1450 transition: background-color var(--transition-base), border-color var(--transition-base); 1451 height: 100%; 1452 box-sizing: border-box; 1453} 1454 1455.card-title { 1456 margin: 0px !important; 1457 font-size: 1.15rem !important; 1458 line-height: 1.4 !important; 1459 display: flex; 1460 align-items: center; 1461 font-weight: 600 !important; 1462 color: var(--color-text) !important; 1463 transition: color var(--transition-base); 1464 padding: 0px !important; 1465 border-bottom: none !important; 1466} 1467 1468.main-learn-card header { 1469 display: flex; 1470 flex-direction: column; 1471 gap: var(--gap-lg); 1472 text-align: center;
1473 align-items: center; 1474 background: var(--color-primary); 1475 border-radius: 7px; 1476 height: 220px; 1477 color: white; 1478 justify-content: center; 1479 margin-bottom: 20px; 1480 display: none; 1481} 1482 1483.card-description { 1484 margin: 0px 0px !important; 1485 color: var(--color-text) !important; 1486 transition: color var(--transition-base); 1487} 1488 1489a.card-button { 1490 color: var(--color-text-contrast); 1491 display: block; 1492 text-decoration: none; 1493 transition: background-color var(--transition-base), color var(--transition-base); 1494 cursor: pointer; 1495 margin: 10px; 1496} 1497 1498a.card-button:hover { 1499 background-color: var(--color-primary-light); 1500} 1501 1502.main-learn-card footer { 1503 width: fit-content; 1504 color: black; 1505} 1506 1507.card-body { 1508 padding: 30px 60px; 1509} 1510 1511@media (max-width: 768px) { 1512 .wrap { 1513 padding-top: 20px; 1514 } 1515 1516 .main-learn-card { 1517 flex-direction: column; 1518 } 1519 1520 .card-body { 1521 padding: 10px; 1522 } 1523} 1524 1525.main-learn-card .read-more { 1526 border: none; 1527 background: none !important; 1528 color: var(--color-primary); 1529} 1530 1531.main-learn-card .read-more:hover { 1532 border-bottom: 0px; 1533 background-color: var(--color-primary-light) !important; 1534} 1535 1536.main-learn-card .read-more svg { 1537 fill: var(--color-primary) !important; 1538} 1539 1540.main-learn-card:hover .read-more svg { 1541 transform: translateX(4px); 1542 opacity: 1; 1543} 1544 1545.main-learn-card .read-more:hover { 1546 background: none !important; 1547} 1548 1549.item-tag { 1550 background: #f1f5f9; 1551 color: #64748b; 1552 padding: 4px 12px; 1553 border-radius: 16px; 1554 font-size: 0.8rem; 1555 font-weight: 500; 1556} 1557 1558.tags { 1559 display: flex; 1560 gap: 15px; 1561 padding-top: 10px; 1562 margin-top: auto; 1563 flex-wrap: wrap; 1564} 1565 1566.dark-theme .item-tag { 1567 color: var(--color-text); 1568 background: var( 1569 --color-bg); 1570} 1571 1572@media (max-width: 768px) { 1573 .wrap { 1574 padding-top: 20px; 1575 } 1576 1577 .card-body { 1578 padding: 10px; 1579 } 1580} 1581 1582@media (max-width: 1024px) { 1583 .card-grid { 1584 display: flex; 1585 flex-direction: column; 1586 gap: 20px; 1587 } 1588 1589 .main-learn-card { 1590 display: flex; 1591 flex-direction: column; 1592 } 1593} 1594</style> 1595<style> 1596.read-more { 1597 font-weight: bold; 1598 text-transform: uppercase; 1599 font-size: var(--fs-sm); 1600 display: flex; 1601 align-items: center; 1602 gap: 5px; 1603 color: var(--color-text); 1604 margin-top: auto; 1605} 1606 1607.read-more svg { 1608 fill: var(--color-text) !important; 1609 transition: transform 0.2s, opacity 0.2s; 1610 opacity: 1; 1611} 1612 1613.read-more:hover svg { 1614 transform: translateX(4px); 1615 opacity: 1; 1616} 1617</style> 1618<style> 1619.code-gallery-tip { 1620 display: none; 1621 align-items: center; 1622 gap: 20px; 1623 color: var(--color-text-light); 1624 justify-content: space-between; 1625 width: 100%; 1626} 1627 1628.code-gallery-tip.active { 1629 display: flex; 1630} 1631 1632.code-gallery-box { 1633 background-color: var(--color-white); 1634 border: 2px solid var(--color-primary); 1635 border-radius: var(--radius-lg); 1636 display: flex; 1637 flex-direction: column; 1638 position: relative; 1639 overflow: hidden; 1640 box-shadow: 1641 0px 124px 74px rgba(35, 55, 139, 0.01), 1642 0px 55px 55px rgba(35, 55, 139, 0.04), 1643 0px 0px 4px rgba(208, 241, 255, 0.25); 1644 width: 100%; 1645 box-sizing: border-box; 1646 height: 515px; 1647} 1648 1649.code-gallery-tabs { 1650 display: flex; 1651 position: relative; 1652 overflow-x: auto; 1653} 1654 1655.code-gallery-tab { 1656 padding: var(--space-3) var(--space-8); 1657 background-color: var(--color-white); 1658 border-bottom: 2px solid var(--color-border); 1659 cursor: pointer; 1660 white-space: nowrap; 1661} 1662 1663.code-gallery-tab.active { 1664 color: var(--color-primary); 1665} 1666 1667.code-gallery-tab.filler { 1668 flex: 1; 1669} 1670 1671.code-gallery-tab-border { 1672 position: absolute; 1673 bottom: 0; 1674 height: 2px; 1675 background: var(--color-primary); 1676 transition: left 0.3s ease, width 0.3s ease; 1677 z-index: 0; 1678} 1679 1680.code-gallery-content { 1681 font-family: monospace; 1682 font-size: 0.9rem; 1683 flex: 1; 1684 line-height: 1.7; 1685 min-height: 300px; 1686 position: relative; 1687 overflow: auto; 1688} 1689 1690.code-gallery-snippet.visible-code { 1691 padding: var(--space-4); 1692 display: block; 1693} 1694 1695.code-gallery-snippet { 1696 display: none; 1697} 1698 1699.code-gallery-footer { 1700 min-height: 70px; 1701 border-top: 1px solid var(--color-border); 1702 display: flex; 1703 padding: 10px 30px; 1704 align-items: center; 1705 gap: 10px; 1706 justify-content: space-between; 1707} 1708 1709.hero-footer-left { 1710 display: flex; 1711 gap: var(--gap-md); 1712 line-height: 1.4; 1713 width: 100%; 1714} 1715 1716.code-gallery-next { 1717 position: absolute; 1718 bottom: -2rem; 1719 right: var(--space-4); 1720 padding: 0.3rem 0.8rem; 1721 border: 1px solid var(--color-primary); 1722 border-radius: var(--radius-sm); 1723 background: var(--color-white); 1724 color: var(--color-primary); 1725 font-weight: bold; 1726 display: flex; 1727 align-items: center; 1728 justify-content: center; 1729 cursor: pointer; 1730} 1731 1732.code-block-wrapper { 1733 position: relative; 1734} 1735 1736.hl.lean span { 1737 color: var(--color-text) !important; 1738} 1739 1740</style> 1741<style> 1742.archive-content { 1743 display: flex; 1744 flex-direction: column; 1745 gap: 15px; 1746 transition: background-color var(--transition-base), border-color var(--transition-base); 1747 padding: var(--space-12); 1748} 1749 1750.archive-content .metadata { 1751 display: flex; 1752 gap: 0px; 1753 font-size: var(--fs-sm); 1754 color: var(--color-text-light); 1755} 1756 1757.archive-content .metadata :not(:last-child)::after { 1758 content: "·"; 1759 margin-left: 0.5rem; 1760} 1761
1762.use-cases-grid ul.post-list { 1763 display: grid; 1764 grid-template-columns: calc(50% - 25px) calc(50% - 25px); 1765} 1766 1767@media (max-width: 1024px) { 1768 .use-cases-grid ul.post-list { 1769 display: flex; 1770 } 1771} 1772 1773/* Fix */ 1774 1775.features-heading { 1776 gap: 70px; 1777 display: flex; 1778 flex-direction: column; 1779} 1780 1781 1782ul.post-list { 1783 padding-bottom: 100px; 1784 display: flex; 1785 flex-direction: column; 1786 gap: 20px; 1787 padding: 0px !important; 1788 margin: 0px !important; 1789 margin-top: 3.5rem !important; 1790} 1791 1792.post-list li { 1793 background-color: var(--card-bg); 1794 border: 1px solid var(--color-border-light); 1795 border-radius: var(--radius-md); 1796 overflow: hidden; 1797 font-size: var(--fs-md); 1798 transition: background-color var(--transition-base), border-color var(--transition-base); 1799} 1800 1801.title span.name { 1802 line-height: 1.2; 1803 font-size: 1.3rem; 1804 font-weight: bold; 1805 color: var(--color-text); 1806 transition: color var(--transition-base); 1807} 1808 1809.post-list li a { 1810 color: var(--color-text) !important; 1811 transition: color var(--transition-base); 1812 border: none !important; 1813 background: none !important; 1814} 1815 1816.page-content { 1817 padding-bottom: 0; 1818} 1819 1820a.read-more { 1821 font-weight: bold; 1822 text-transform: uppercase; 1823 font-size: var(--fs-sm); 1824 display: flex; 1825 align-items: center; 1826 gap: 5px; 1827} 1828 1829.post-list li, .post-list p { 1830 color: var(--color-text-light) !important; 1831 line-height: 1.6 !important; 1832 margin: 0px !important; 1833} 1834 1835.metadata { 1836 display: flex; 1837 gap: 0px; 1838 font-size: var(--fs-sm); 1839 color: var(--color-text-light); 1840} 1841 1842.metadata :not(:last-child)::after { 1843 content: "·"; 1844 margin-left: 0.5rem; 1845} 1846 1847.post-list li:hover .read-more svg { 1848 transform: translateX(4px); 1849 opacity: 1; 1850} 1851 1852.blog-page { 1853 padding-top: 0px !important 1854} 1855 1856@media (max-width: 768px) { 1857 .wrap { 1858 padding-top: var(--space-8); 1859 } 1860 1861 .title span.name { 1862 font-size: var(--fs-lg); 1863 } 1864 1865} 1866 1867.archive-content { 1868 display: flex; 1869 flex-direction: column; 1870 gap: 15px; 1871 transition: background-color var(--transition-base), border-color var(--transition-base); 1872 padding: var(--space-12); 1873} 1874 1875.post-list li img { 1876 height: 200px; 1877 object-fit: cover; 1878 width: 100%; 1879 margin: 0px; 1880 border-radius: 0px; 1881 box-shadow: none; 1882} 1883</style> 1884<style> 1885 1886 @media (scripting: none) { 1887 #selector-input---verso-component-5-1:checked ~ .selector-list .selector-button[for="selector-input---verso-component-5-1"] { 1888 background-color: var(--color-primary); 1889 color: white; 1890 } 1891 1892 #--verso-component-5-panel-1 { 1893 display: none; 1894 } 1895 1896 #selector-input---verso-component-5-1:checked ~ .selector-panels > #--verso-component-5-panel-1 { 1897 display: block; 1898 } 1899 } 1900 1901</style> 1902<style> 1903.gallery-card-content, 1904.gallery-card-image { 1905 flex: 1; 1906} 1907 1908.gallery-card-content { 1909 padding: var(--space-12); 1910 display: flex; 1911 flex-direction: column; 1912 justify-content: start; 1913 gap: 20px; 1914} 1915 1916.gallery-tag { 1917 font-size: var(--fs-xs); 1918 font-weight: bold; 1919 color: var(--color-text-contrast); 1920 text-transform: uppercase; 1921 background: var(--color-primary); 1922 width: fit-content; 1923 padding: var(--space-1) var(--space-6); 1924 border-radius: var(--radius-pill); 1925} 1926 1927.gallery-title { 1928 font-size: var(--fs-xl); 1929 font-weight: 700; 1930 color: var(--color-text); 1931} 1932 1933.gallery-description { 1934 font-size: var(--fs-md); 1935 color: var(--color-text-light); 1936 line-height: 1.4; 1937} 1938 1939.gallery-card-image img { 1940 width: 100%; 1941 height: 100%; 1942 object-fit: cover; 1943 display: block; 1944} 1945 1946@media (max-width: 768px) { 1947 .gallery-card-image { 1948 display: none; 1949 } 1950} 1951 1952.gallery-body { 1953 grid-template-columns: repeat(2, minmax(0, 1fr)); 1954 width: 100%; 1955 overflow: hidden; 1956 background-color: var(--color-white); 1957 display: grid; 1958 height: 100%; 1959} 1960 1961.gallery-body.active { 1962 display: grid !important; 1963} 1964 1965.gallery-body:hover .read-more svg { 1966 transform: translateX(4px); 1967 opacity: 1; 1968} 1969 1970@media (max-width: 768px) { 1971 .gallery-body { 1972 grid-template-columns: repeat(1, minmax(0, 1fr)); 1973 } 1974} 1975 1976.selector-panels { 1977 max-width: 100%; 1978 width: 100%; 1979 display: grid;
1980 grid-template-areas: "slide"; 1981} 1982 1983.selector-button p { 1984 text-align: center; 1985} 1986</style> 1987<style> 1988.feature { 1989 flex: 1; 1990 padding: var(--space-6); 1991 transition: all var(--transition-fast); 1992 display: flex; 1993 flex-direction: column; 1994 min-width: 200px; 1995} 1996 1997.feature-title { 1998 display: flex; 1999 align-items: center; 2000 gap: var(--space-3); 2001 font-weight: 600; 2002 font-size: var(--fs-md); 2003 margin-bottom: var(--space-6); 2004} 2005 2006.feature-description { 2007 font-size: var(--fs-base); 2008 line-height: 1.4; 2009 flex-grow: 1; 2010 display: flex; 2011 justify-content: center; 2012 align-items: flex-start; 2013 color: var(--color-text-light); 2014} 2015 2016.features-heading { 2017 gap: 70px; 2018 display: flex; 2019 flex-direction: column; 2020} 2021</style> 2022<style> 2023 summary { 2024 font-weight: bold; 2025 cursor: pointer; 2026 list-style: none; 2027 display: flex; 2028 align-items: center; 2029 justify-content: space-between; 2030} 2031 2032.accordion summary::-webkit-details-marker { 2033 display: none; 2034} 2035 2036.accordion summary::after { 2037 content: "â¶"; 2038 display: inline-block; 2039 margin-left: 0.5em; 2040 transition: transform 0.2s ease; 2041} 2042 2043details.accordion[open] summary::after { 2044 transform: rotate(90deg); 2045} 2046 2047details.accordion { 2048 border-bottom: 1px solid var(--color-border); 2049} 2050 2051</style> 2052<style> 2053 2054 @media (scripting: none) { 2055 #selector-input---verso-component-5-4:checked ~ .selector-list .selector-button[for="selector-input---verso-component-5-4"] { 2056 background-color: var(--color-primary); 2057 color: white; 2058 } 2059 2060 #--verso-component-5-panel-4 { 2061 display: none; 2062 } 2063 2064 #selector-input---verso-component-5-4:checked ~ .selector-panels > #--verso-component-5-panel-4 { 2065 display: block; 2066 } 2067 } 2068 2069</style> 2070<style> 2071 2072 @media (scripting: none) { 2073 #selector-input---verso-component-28-0:checked ~ .selector-list .selector-button[for="selector-input---verso-component-28-0"] { 2074 background-color: var(--color-primary); 2075 color: white; 2076 } 2077 2078 #--verso-component-28-panel-0 { 2079 display: none; 2080 } 2081 2082 #selector-input---verso-component-28-0:checked ~ .selector-panels > #--verso-component-28-panel-0 { 2083 display: block; 2084 } 2085 } 2086 2087</style> 2088<style> 2089#main-background { 2090 position: absolute; 2091 right: 0px; 2092 top: 0px; 2093} 2094 2095.background-wrapper { 2096 z-index: var(--z-below); 2097 width: min(1400px, 100vw); 2098} 2099 2100.background-wrapper svg { 2101 width: 100%; 2102 stroke: #D7E0E9; 2103} 2104 2105.dark-theme .background-wrapper svg { 2106 stroke: #1C1E26; 2107} 2108</style> 2109<style> 2110 2111 @media (scripting: none) { 2112 #selector-input---verso-component-28-2:checked ~ .selector-list .selector-button[for="selector-input---verso-component-28-2"] { 2113 background-color: var(--color-primary); 2114 color: white; 2115 } 2116 2117 #--verso-component-28-panel-2 { 2118 display: none; 2119 } 2120 2121 #selector-input---verso-component-28-2:checked ~ .selector-panels > #--verso-component-28-panel-2 { 2122 display: block; 2123 } 2124 } 2125 2126</style> 2127<style> 2128 2129 @media (scripting: none) { 2130 #selector-input---verso-component-5-5:checked ~ .selector-list .selector-button[for="selector-input---verso-component-5-5"] { 2131 background-color: var(--color-primary); 2132 color: white; 2133 } 2134 2135 #--verso-component-5-panel-5 { 2136 display: none; 2137 } 2138 2139 #selector-input---verso-component-5-5:checked ~ .selector-panels > #--verso-component-5-panel-5 { 2140 display: block; 2141 } 2142 } 2143 2144</style> 2145<style> 2146.selector-list { 2147 display: grid; 2148 grid-auto-flow: column; 2149 grid-auto-columns: 1fr; 2150 gap: var(--gap-sm); 2151 padding: var(--space-4); 2152 width: fit-content; 2153 position: relative; 2154 max-width: 100%; 2155 overflow-x: auto; 2156 box-sizing: border-box; 2157} 2158 2159@media (max-width: 768px) { 2160 .selector-list { 2161 width: 100%; 2162 } 2163} 2164 2165.selector-button { 2166 padding: var(--space-2) var(--space-6); 2167 border-radius: var(--radius-md); 2168 background: transparent; 2169 color: var(--color-text); 2170 border: none; 2171 cursor: pointer; 2172 font-weight: 500; 2173 font-size: var(--fs-base); 2174 position: relative; 2175 z-index: var(--z-above); 2176 transition: background var(--transition-fast), color var(--transition-fast); 2177 text-align: center; 2178 white-space: pre; 2179} 2180 2181.selector-button:hover { 2182 background: #7094de1c; 2183} 2184 2185.selector-button.active { 2186 color: var(--color-text-contrast); 2187} 2188 2189@media (scripting: none) { 2190 .selector-button.active { 2191 background-color: var(--color-primary); 2192 } 2193} 2194 2195.selector-group::before { 2196 content: ''; 2197 position: absolute; 2198 top: 0; 2199 left: 0; 2200 width: 0; 2201 height: 100%; 2202 background: var(--color-primary-light); 2203 border-radius: var(--radius-md); 2204 transition: left var(--transition-base), width var(--transition-base); 2205 z-index: var(--z-normal); 2206} 2207 2208.selector-panel { 2209 display: none; 2210 width: 100%; 2211 min-width: 0; 2212} 2213 2214.selector-panel.active { 2215 display: block; 2216} 2217 2218.selector-panel.same-size { 2219 display: block; 2220 grid-area: slide; 2221 visibility: hidden; 2222 width: 100%; 2223} 2224 2225.selector-panel.same-size.active { 2226 visibility: visible; 2227} 2228 2229.selector-panel > article { 2230 height: 100%; 2231} 2232 2233.selectors-container { 2234 gap: var(--gap-lg); 2235 display: flex; 2236 align-items: center; 2237 flex-direction: column; 2238 max-width: 100vw; 2239} 2240 2241.active-background { 2242 position: absolute; 2243 height: 34px; 2244 background: var(--color-primary); 2245 border-radius: var(--radius-md); 2246 z-index: var(--z-normal); 2247} 2248</style> 2249<style> 2250 2251 .custom-subtitle { 2252 padding: 0px; 2253 font-size: 1.5rem !important; 2254 margin: 0px !important; 2255 border: none !important; 2256 font-weight: normal !important; 2257 color: #868686 !important; 2258 font-style: italic; 2259 } 2260 2261 @media (max-width: 768px) { 2262 .custom-subtitle { 2263 padding-top: 20px; 2264 font-size: 1.4rem !important; 2265 } 2266 } 2267 2268</style> 2269<style> 2270.copy-button { 2271 position: absolute; 2272 top: 8px; 2273 right: 8px; 2274 padding: 6px 12px; 2275 font-size: 0.8em; 2276 cursor: pointer; 2277 z-index: 10; 2278 opacity: 0; 2279 transition: 0.2s opacity; 2280 border: 1px solid var(--color-border); 2281 background: var(--color-bg); 2282 border-radius: 5px; 2283 color: var(--color-text); 2284} 2285 2286.code-block-wrapper:hover .copy-button { 2287 opacity: 1; 2288} 2289 2290.hero .copy-button { 2291 right: 0px; 2292 top: 0px; 2293} 2294</style> 2295<style> 2296.hero { 2297 display: flex; 2298 flex-direction: column; 2299 justify-content: space-between; 2300 box-sizing: border-box; 2301 width: 100%; 2302 padding: 0; 2303 padding-top: var(--space-6); 2304} 2305 2306.hero-content { 2307 display: grid; 2308 gap: var(--space-8); 2309 align-items: center; 2310 flex-wrap: wrap; 2311 justify-content: space-between; 2312 margin: var(--space-4); 2313 grid-template-columns: 40% 50%; 2314} 2315 2316.hero-left { 2317 display: flex; 2318 flex-direction: column; 2319 width: 100%; 2320 justify-content: space-between; 2321} 2322 2323.hero-branding { 2324 display: flex; 2325 flex-direction: column; 2326 gap: var(--gap-lg); 2327 max-width: 100%; 2328} 2329 2330.hero-logo { 2331 width: 300px; 2332} 2333 2334.hero-tagline { 2335 margin-top: var(--space-2); 2336 font-size: var(--fs-md); 2337 color: var(--color-muted); 2338 line-height: 1.4; 2339 font-weight: 400; 2340} 2341 2342.hero-tagline span { 2343 color: var(--color-primary); 2344 font-weight: 500; 2345} 2346 2347.hero-buttons { 2348 display: flex; 2349 gap: var(--space-4); 2350 margin-top: var(--space-8); 2351 background-color: transparent; 2352} 2353 2354.hero-buttons a { 2355 width: 170px; 2356} 2357 2358.hero-buttons a.primary svg { 2359 fill: var(--color-text-contrast); 2360} 2361 2362.learn-button, 2363.install-button { 2364 position: relative; 2365} 2366 2367.learn-button span { 2368 position: relative; 2369 z-index: var(--z-above); 2370 display: flex; 2371 gap: var(--space-2); 2372 align-items: center; 2373} 2374 2375.learn-button span svg { 2376 transition: all var(--transition-base); 2377} 2378 2379.hero-right { 2380 position: relative; 2381} 2382 2383.hero-bottom { 2384 margin: var(--space-4); 2385 margin-top: var(--space-12); 2386 background-color: var(--color-white); 2387 border: 2px solid var(--color-primary); 2388 border-radius: var(--radius-lg); 2389 display: flex; 2390 box-shadow: 0px 35px 77px rgba(9, 62, 185, 0.10), 0px 140px 140px rgba(9, 62, 185, 0.09); 2391 justify-content: space-between; 2392 flex-wrap: wrap; 2393 box-shadow: 2394 0px 35px 77px rgba(9, 62, 185, 0.10), 2395 0px 140px 140px rgba(9, 62, 185, 0.09); 2396 padding: var(--space-6); 2397 box-sizing: border-box; 2398} 2399 2400.scroll-btn { 2401 position: absolute; 2402 background: rgb(0 0 0 / 10%); 2403 color: #ffffff; 2404 pointer-events: none; 2405 transition: opacity 0.3s ease; 2406 user-select: none; 2407 font-size: 1.2em; 2408 height: 100%; 2409 width: 50px; 2410 border: honeydew; 2411 border-radius: 0 !important; 2412 opacity: 0; 2413} 2414 2415.scroll-btn.right { 2416 right: 0; 2417} 2418
2419.code-gallery-content:hover .scroll-btn { 2420 opacity: 1; 2421 pointer-events: auto; 2422} 2423 2424.code-gallery-content * { 2425 overflow: auto; 2426} 2427 2428.hero-radial-blur { 2429 position: absolute; 2430 inset: 0; 2431 background: radial-gradient(farthest-side ellipse at center, #437ef78a 0%, rgba(255, 255, 255, 0) 80%); 2432 z-index: var(--z-below); 2433 width: 1000px; 2434 height: 1000px; 2435 left: calc((1070px - 600px) / 2 * -1); 2436 top: calc((900px - 500px) / 2 * -1); 2437 opacity: 60%; 2438 pointer-events: none; 2439} 2440 2441.projects-section { 2442 position: relative; 2443 overflow: visible; 2444} 2445 2446.projects-section .hero-radial-blur { 2447 left: 50%; 2448 top: 60%; 2449 transform: translate(-50%, -50%); 2450 width: 900px; 2451 height: 900px; 2452 opacity: 50%; 2453} 2454 2455.page-content { 2456 padding-top: 70px; 2457 display: flex; 2458 flex-direction: column; 2459 gap: var(--gap-xl); 2460 padding-bottom: var(--space-12); 2461} 2462 2463.read-more { 2464 font-weight: bold; 2465 text-transform: uppercase; 2466 font-size: var(--fs-sm); 2467 display: flex; 2468 align-items: center; 2469 gap: 5px; 2470 color: var(--color-text); 2471 margin-top: auto; 2472} 2473 2474.read-more svg { 2475 fill: var(--color-text) !important; 2476 transition: transform 0.2s, opacity 0.2s; 2477 opacity: 1; 2478} 2479 2480.read-more:hover svg { 2481 transform: translateX(4px); 2482 opacity: 1; 2483} 2484 2485.code-gallery-content .token, .code-gallery-content .inter-text { 2486 opacity: 0; 2487 animation: fadeInCode 0.3s ease forwards; 2488} 2489 2490@keyframes fadeIn { 2491 0% { 2492 opacity: 0; 2493 top: -20px; 2494 } 2495 100% { 2496 opacity: 1; 2497 top: 0; 2498 } 2499} 2500 2501@keyframes fadeInCode { 2502 0% { 2503 opacity: 0; 2504 } 2505 100% { 2506 opacity: 1; 2507 } 2508} 2509 2510@media (max-width: 1024px) { 2511 .hero-left { 2512 width: 100%; 2513 } 2514 2515 .code-gallery-box, 2516 .hero-right { 2517 width: 100%; 2518 } 2519 2520 .hero-content { 2521 display: flex; 2522 justify-content: center; 2523 padding: 20px; 2524 } 2525 2526 .hero-left { 2527 display: flex; 2528 align-items: center; 2529 flex-direction: row; 2530 } 2531 2532 .code-gallery-box, 2533 .hero-right { 2534 width: 100%; 2535 } 2536 2537 .hero-buttons a { 2538 padding: var(--space-4) var(--space-12); 2539 } 2540 2541 .hero-bottom { 2542 margin: var(--space-4); 2543 margin-top: var(--space-12); 2544 } 2545 2546 .hero-content { 2547 gap: 70px; 2548 } 2549 2550 .hero-buttons { 2551 display: flex; 2552 flex-direction: column; 2553 width: 100%; 2554 padding: 0 var(--gap-lg); 2555 box-sizing: border-box; 2556 margin: 0; 2557 } 2558 2559 .hero-buttons a { 2560 width: auto; 2561 height: 100%; 2562 } 2563 2564 .sponsors { 2565 width: calc(100% - var(--space-8)*2); 2566 } 2567} 2568 2569@media (max-width: 768px) { 2570 .hero { 2571 padding: var(--space-4); 2572 padding-top: var(--space-1); 2573 gap: 30px; 2574 } 2575 2576 .feature { 2577 min-width: auto; 2578 padding: var(--space-4); 2579 } 2580 2581 .hero-bottom { 2582 margin: 0px; 2583 } 2584 2585 .hero-tagline { 2586 text-align: center; 2587 } 2588 2589 .hero-left { 2590 width: 100%; 2591 flex-direction: column; 2592 } 2593 2594 .hero-radial-blur { 2595 display: none; 2596 } 2597 2598 .code-gallery-box, 2599 .hero-right { 2600 width: 100%; 2601 box-sizing: border-box; 2602 } 2603 2604 .hero-branding { 2605 display: flex; 2606 align-items: center; 2607 } 2608 2609 .hero-content { 2610 margin: 0px; 2611 justify-content: center; 2612 gap: 30px; 2613 padding: 0px; 2614 padding-top: 30px; 2615 } 2616 2617 .hero-buttons a { 2618 width: auto; 2619 } 2620 2621 .hero-buttons { 2622 flex-wrap: wrap; 2623 width: 100%; 2624 padding: 0; 2625 margin-top: 50px; 2626 } 2627 2628 .sponsors-content { 2629 justify-content: center; 2630 flex-direction: column; 2631 width: 100%; 2632 } 2633} 2634 2635#banner { 2636 background: var(--color-primary); 2637 color: var(--color-text-contrast); 2638 padding: 30px; 2639 text-align: center; 2640 text-transform: uppercase; 2641 margin-bottom: 20px; 2642} 2643 2644#banner a { 2645 color: var(--color-text-contrast); 2646 border-bottom: 1px solid var(--color-text-contrast); 2647} 2648 2649.hero-branding svg { 2650 max-width: 100%; 2651} 2652 2653.code-gallery-run { 2654 height: 40px; 2655 width: 40px; 2656 border: 2px solid #5185F4; 2657 box-sizing: border-box; 2658 display: flex; 2659 flex-shrink: 0; 2660 align-items: center; 2661 border-radius: 5px; 2662 justify-content: center; 2663 transition: background 0.2s; 2664} 2665 2666.code-gallery-run svg { 2667 transition: background 0.2s; 2668} 2669 2670.code-gallery-run:hover { 2671 background: #5185F4; 2672} 2673 2674.code-gallery-run:hover svg { 2675 fill: #ffffff; 2676} 2677 2678.code-gallery-tab { 2679 font-size: 0.85rem; 2680 font-weight: 500; 2681 color: var(--color-text-light); 2682} 2683 2684@media (max-width: 830px) { 2685 .hero-bottom { 2686 flex-direction: column; 2687 } 2688} 2689 2690#page { 2691 display: flex; 2692 flex-direction: column; 2693 padding-bottom: 100px; 2694 flex-grow: 1; 2695 gap: 100px; 2696 max-width: 100vw; 2697} 2698 2699@media (max-width: 768px) { 2700 #page { 2701 padding-top: 20px; 2702 gap: 50px; 2703 } 2704} 2705 2706.dark-theme:root .hero-branding svg { 2707 stroke: white; 2708} 2709</style> 2710<style> 2711.error-container { 2712 display: flex; 2713 flex-direction: row; 2714 gap: 4rem;
2715 align-items: center; 2716 justify-content: center; 2717 flex-wrap: wrap; 2718 padding: 150px; 2719 padding-top: 150px; 2720 padding-bottom: 50px; 2721 box-sizing: border-box; 2722} 2723 2724.error-container .image-section { 2725 flex: 1; 2726 display: flex; 2727 justify-content: center; 2728 align-items: center; 2729 min-width: 300px; 2730} 2731 2732.error-container .image-section img { 2733 width: min(400px, 100%); 2734 height: min(400px, 100%); 2735 max-width: 400px; 2736 max-height: 400px; 2737 display: flex; 2738 align-items: center; 2739 justify-content: center; 2740 text-align: center; 2741 box-sizing: border-box; 2742} 2743 2744.error-container .image-section img { 2745 width: min(400px, 100%); 2746 height: min(400px, 100%); 2747 max-width: 400px; 2748 max-height: 400px; 2749 display: flex; 2750 align-items: center; 2751 justify-content: center; 2752 text-align: center; 2753 box-sizing: border-box; 2754} 2755 2756.text-section { 2757 flex: 1; 2758 display: flex; 2759 flex-direction: column; 2760 gap: 1.25rem; 2761 padding: 1rem; 2762 min-width: 300px; 2763 max-width: 600px; 2764 text-align: center; 2765} 2766 2767.error-code { 2768 font-size: clamp(3rem, 8vw, 6rem); 2769 font-weight: bold; 2770 line-height: 1; 2771} 2772 2773.error-title { 2774 font-size: clamp(1.5rem, 4vw, 2rem); 2775 color: var(--color-text); 2776 line-height: 1.2; 2777 font-weight: bold; 2778 font-size: 2.3rem; 2779} 2780 2781.error-description { 2782 font-size: clamp(1rem, 2.5vw, 1.125rem); 2783 color: var(--color-text); 2784 line-height: 1.6; 2785 text-align: center; 2786} 2787 2788.action-buttons { 2789 margin-top: 1rem; 2790 display: flex; 2791 justify-content: center; 2792} 2793 2794 2795@media (max-width: 768px) { 2796 .error-container { 2797 flex-direction: column; 2798 gap: 1.5rem; 2799 padding: 2rem; 2800 padding-top: 3rem; 2801 text-align: center; 2802 } 2803 2804 .image-section, 2805 .text-section { 2806 flex: none; 2807 width: 100%; 2808 min-width: unset; 2809 } 2810 2811 .octopus-placeholder { 2812 width: min(300px, calc(100vw - 4rem), 40vw); 2813 height: min(300px, calc(100vw - 4rem), 40vw); 2814 } 2815 2816 .text-section { 2817 gap: 1rem; 2818 padding: 0px; 2819 } 2820} 2821 2822</style> 2823<style> 2824 2825 @media (scripting: none) { 2826 #selector-input---verso-component-5-3:checked ~ .selector-list .selector-button[for="selector-input---verso-component-5-3"] { 2827 background-color: var(--color-primary); 2828 color: white; 2829 } 2830 2831 #--verso-component-5-panel-3 { 2832 display: none; 2833 } 2834 2835 #selector-input---verso-component-5-3:checked ~ .selector-panels > #--verso-component-5-panel-3 { 2836 display: block; 2837 } 2838 } 2839 2840</style> 2841<style> 2842.heading-section { 2843 text-align: center; 2844 display: flex; 2845 flex-direction: column; 2846 align-items: center; 2847 gap: var(--space-3); 2848 margin-bottom: var(--space-8); 2849} 2850 2851.heading-section > span { 2852 display: inline-flex; 2853 align-items: center; 2854 font-size: 0.72rem; 2855 font-weight: 700; 2856 letter-spacing: 0.13em; 2857 text-transform: uppercase; 2858 padding: 5px 16px; 2859 border-radius: var(--radius-pill); 2860 border: 1px solid transparent; 2861} 2862 2863/* Default / primary: solid primary colour pill, white text */ 2864.heading-section > span.badge-primary { 2865 background: var(--color-primary); 2866 color: var(--color-text-contrast); 2867 border-color: transparent; 2868} 2869 2870/* Secondary: glassmorphic â for use on coloured/dark backgrounds */ 2871.heading-section > span.badge-secondary { 2872 background: rgba(255, 255, 255, 0.12); 2873 color: rgba(255, 255, 255, 0.90); 2874 border-color: rgba(255, 255, 255, 0.22); 2875 backdrop-filter: blur(8px); 2876 -webkit-backdrop-filter: blur(8px); 2877} 2878 2879.heading-title { 2880 font-size: var(--fs-2xl); 2881 font-weight: 700; 2882 font-family: var(--font-primary); 2883 letter-spacing: -0.02em; 2884 line-height: 1.1; 2885 margin: var(--space-2) 0 0; 2886 color: var(--color-text); 2887 transition: color var(--transition-base); 2888} 2889 2890.heading-subtitle { 2891 font-size: var(--fs-md); 2892 color: var(--color-text-light); 2893 margin-top: var(--space-2); 2894 line-height: 1.55; 2895 transition: color var(--transition-base); 2896 max-width: 600px; 2897} 2898 2899.page-title { 2900 font-size: 2.5rem !important; 2901 margin-top: 4rem; 2902 font-weight: bold; 2903 text-align: left; 2904 padding: 0px !important; 2905 margin: 0px !important; 2906} 2907 2908@media (max-width: 768px) { 2909 .heading-title { 2910 font-size: 2rem; 2911 } 2912} 2913</style> 2914<style> 2915.no-js-warning { 2916 position: sticky; 2917 top: 0; 2918 width: 100%; 2919 background-color: red; 2920 color: white; 2921 text-align: center; 2922 padding: 0.75em; 2923 font-family: sans-serif; 2924 font-size: 1em; 2925 z-index: 9999; 2926} 2927</style> 2928<style> 2929.button-container { 2930 display: flex; 2931 gap: 10px; 2932 margin: 30px 0px; 2933} 2934 2935@media (max-width: 768px) { 2936 .button-container { 2937 flex-direction: column; 2938 } 2939} 2940 2941.btn { 2942 white-space: nowrap; 2943 display: flex; 2944 align-items: center; 2945 justify-content: center; 2946 gap: 5px; 2947 padding: 10px 30px; 2948 background-color: #3498db; 2949 color: white; 2950 border: none; 2951 border-radius: 5px; 2952 cursor: pointer; 2953 font-size: 16px; 2954 flex: 1; 2955 background: var(--card-bg) !important; 2956 border: 1px solid var(--color-border) !important; 2957 color: var(--color-text) !important; 2958 gap: 10px; 2959} 2960</style> 2961<style> 2962.modal-backdrop { 2963 max-height: 100vh; 2964 position: fixed; 2965 top: 0; 2966 left: 0; 2967 width: 100vw; 2968 height: 100vh; 2969 background-color: rgba(0, 0, 0, 0.75); 2970 display: flex; 2971 align-items: center; 2972 justify-content: center; 2973 z-index: 9999; 2974} 2975 2976.modal { 2977 background: var(--color-white); 2978 padding: 2rem; 2979 border-radius: 0.5rem; 2980 max-width: 500px; 2981 width: 90%; 2982 position: relative; 2983 box-shadow: 0 2px 10px rgba(0, 0, 0, 0.2); 2984 max-height: calc(100vh - 40px); 2985 box-sizing: border-box; 2986 overflow: auto; 2987 display: flex; 2988 flex-wrap: wrap; 2989 width: 100%; 2990 transform-origin: center; 2991 will-change: transform, opacity; 2992} 2993 2994.modal-close { 2995 color: var(--color-text); 2996 position: absolute; 2997 top: 0.5rem; 2998 right: 0.75rem; 2999 background: none; 3000 border: none; 3001 font-size: 1.5rem; 3002 cursor: pointer; 3003} 3004 3005.hidden { 3006 display: none; 3007} 3008 3009body.modal-open { 3010 overflow: hidden; 3011} 3012 3013/* Modal for Step 2 */ 3014 3015.modal-content { 3016 padding: 2rem; 3017 border-radius: 1rem; 3018} 3019 3020.modal-content h2 { 3021 font-size: 1.5rem; 3022 margin-bottom: 0.5rem; 3023 font-weight: 600; 3024 padding-left: 0.5rem; 3025 text-align: center; 3026 margin: 0px !important; 3027} 3028 3029.steps { 3030 display: flex; 3031 flex-direction: column; 3032 gap: 2rem; 3033 margin-top: 2rem; 3034} 3035
3036.step .screenshot, .step .gallery-item { 3037 width: 120px; 3038} 3039 3040.step { 3041 display: flex; 3042 gap: 1rem; 3043 align-items: center; 3044 transition: transform 0.2s ease-in-out; 3045} 3046 3047.step img { 3048 width: 120px !important; 3049 height: 120px !important; 3050 object-fit: cover; 3051 border-radius: 0.5rem; 3052 border: 1px solid #444; 3053 margin: 0px; 3054} 3055 3056.step p { 3057 margin: 0; 3058 font-size: 1rem; 3059 line-height: 1.4; 3060} 3061 3062.modal-content a { 3063 text-align: center; 3064 width: 100%; 3065 padding-top: 20px; 3066 box-sizing: border-box; 3067 display: block; 3068 background: none !important; 3069 border: none !important; 3070} 3071 3072@media (max-width: 768px) { 3073 .modal { 3074 border-radius: 0px; 3075 } 3076} 3077</style> 3078<style> 3079 3080 @media (scripting: none) { 3081 #selector-input---verso-component-28-1:checked ~ .selector-list .selector-button[for="selector-input---verso-component-28-1"] { 3082 background-color: var(--color-primary); 3083 color: white; 3084 } 3085 3086 #--verso-component-28-panel-1 { 3087 display: none; 3088 } 3089 3090 #selector-input---verso-component-28-1:checked ~ .selector-panels > #--verso-component-28-panel-1 { 3091 display: block; 3092 } 3093 } 3094 3095</style>
3096<script> 3097 3098document.addEventListener('DOMContentLoaded', () => { 3099 initTabSelectors(); 3100 initAccessibilityTab(); 3101 3102 const shouldChangeDefault = detectOS() && document.querySelector('.device-tabs'); 3103 if (shouldChangeDefault) { 3104 changeTabDefault(); 3105 } 3106 3107 tippy('.code-gallery-run', { 3108 content: "Opens the current code in the playground!", 3109 }); 3110 3111 tippy('.social-icon', { 3112 placement: 'top', 3113 }); 3114 3115}); 3116 3117function observeUntilVisible(element, callback) { 3118 if (!element) return; 3119 3120 const observers = []; 3121 3122 function isElementVisible(el) { 3123 while (el) { 3124 const style = getComputedStyle(el); 3125 if (style.display === 'none' || style.visibility === 'hidden' || style.opacity === '0') { 3126 return false; 3127 } 3128 el = el.parentElement; 3129 } 3130 return true; 3131 } 3132 3133 function disconnectAllObservers(observerList) { 3134 observerList.forEach(observer => observer.disconnect()); 3135 } 3136 3137 const targetObserver = new MutationObserver(() => { 3138 if (isElementVisible(element)) { 3139 callback(); 3140 disconnectAllObservers(observers); 3141 } 3142 }); 3143 3144 targetObserver.observe(element, { 3145 attributes: true, 3146 attributeFilter: ['style', 'class'] 3147 }); 3148 observers.push(targetObserver); 3149 3150 let parent = element.parentElement; 3151 while (parent && parent !== document.body) { 3152 const parentObserver = new MutationObserver(() => { 3153 if (isElementVisible(element)) { 3154 callback(); 3155 disconnectAllObservers(observers); 3156 } 3157 }); 3158 3159 parentObserver.observe(parent, { 3160 attributes: true, 3161 attributeFilter: ['style', 'class'] 3162 }); 3163 observers.push(parentObserver); 3164 3165 parent = parent.parentElement; 3166 } 3167 3168 if (isElementVisible(element)) { 3169 callback(); 3170 disconnectAllObservers(observers); 3171 } 3172} 3173 3174function getHiddenElementRect(element) { 3175 const clone = element.cloneNode(true); 3176 3177 clone.style.position = 'absolute'; 3178 clone.style.visibility = 'hidden'; 3179 clone.style.display = 'block'; 3180 clone.style.top = '-9999px'; 3181 document.body.appendChild(clone); 3182 3183 const rect = clone.getBoundingClientRect(); 3184 document.body.removeChild(clone); 3185 3186 return rect; 3187} 3188 3189function initAccessibilityTab() { 3190 document.querySelectorAll(".selector-button").forEach(button => { 3191 button.addEventListener('keydown', (e) => { 3192 if (e.key === 'Enter') { 3193 e.preventDefault(); 3194 button.click(); 3195 } 3196 }); 3197 }); 3198} 3199 3200function activateTab(button, contentContainer, activeState) { 3201 const { 3202 activeButton, 3203 activePanel 3204 } = activeState; 3205 3206 if (button === activeButton) return; 3207 3208 if (activeButton) { 3209 activeButton.classList.remove('active'); 3210 activeButton.setAttribute('aria-selected', 'false'); 3211 } 3212 3213 button.classList.add('active'); 3214 button.setAttribute('aria-selected', 'true'); 3215 activeState.activeButton = button; 3216 3217 const targetPanel = contentContainer.querySelector(`:scope > .selector-panel[data-id="${button.dataset.id}"]`); 3218 3219 if (activePanel && activePanel !== targetPanel) { 3220 activePanel.classList.remove('active'); 3221 activePanel.setAttribute('aria-hidden', 'true'); 3222 } 3223 3224 if (targetPanel) { 3225 targetPanel.classList.add('active'); 3226 targetPanel.setAttribute('aria-hidden', 'false'); 3227 activeState.activePanel = targetPanel; 3228 } 3229} 3230 3231function setActiveTabByIndex(tabsContainer, index) { 3232 const tabButtons = tabsContainer.querySelectorAll(':scope > .selector-list > .selector-button'); 3233 if (tabButtons.length === 0 || index < 0 || index >= tabButtons.length) return; 3234 3235 const button = tabButtons[index]; 3236 3237 const dataId = tabsContainer.dataset.id; 3238 const contentContainer = document.querySelector(`.selector-panels[data-id="${dataId}"]`); 3239 if (!contentContainer) return; 3240 3241 let activeButton = tabsContainer.querySelector(':scope > .selector-list > .selector-button.active'); 3242 let activePanel = contentContainer.querySelector(':scope > .selector-panel.active'); 3243 const activeState = { 3244 activeButton, 3245 activePanel 3246 }; 3247 3248 activateTab(button, contentContainer, activeState); 3249 3250 const tabList = tabsContainer.querySelector('.selector-list'); 3251 if (tabList) { 3252 requestAnimationFrame(() => { 3253 requestAnimationFrame(() => {
3254 updateTabBackgroundIndicator(tabList, button); 3255 }); 3256 }); 3257 } 3258} 3259 3260function initTabContentPanels(tabsContainer, contentContainer) { 3261 const tabButtons = tabsContainer.querySelectorAll(':scope > .selector-list > .selector-button'); 3262 3263 if (tabButtons.length === 0) return; 3264 3265 let initialButton = tabsContainer.querySelector(':scope > .selector-list > .selector-button[data-initial="true"]'); 3266 if (initialButton) { 3267 initialButton.classList.add('active'); 3268 } 3269 3270 let activeButton = tabsContainer.querySelector(':scope > .selector-list > .selector-button.active'); 3271 let activePanel = contentContainer.querySelector(':scope > .selector-panel.active'); 3272 3273 const activeState = { 3274 activeButton, 3275 activePanel 3276 }; 3277 3278 tabButtons.forEach(button => { 3279 button.setAttribute('role', 'tab'); 3280 button.setAttribute('aria-selected', button === activeButton ? 'true' : 'false'); 3281 3282 button.addEventListener('click', () => { 3283 activateTab(button, contentContainer, activeState); 3284 }); 3285 }); 3286} 3287 3288function setBackgroundPosition(activeBackground, tab) { 3289 tab.offsetHeight; // force reflow 3290 activeBackground.style.left = `${tab.offsetLeft}px`; 3291 activeBackground.style.top = `${tab.offsetTop}px`; 3292 activeBackground.style.width = `${tab.offsetWidth}px`; 3293 activeBackground.style.height = `${tab.offsetHeight}px`; 3294} 3295
3296function springBackgroundPosition(activeBackground, tab) { 3297 const animate = window.Motion?.animate; 3298 if (!animate) { 3299 setBackgroundPosition(activeBackground, tab); 3300 return; 3301 } 3302 animate( 3303 activeBackground, 3304 { left: tab.offsetLeft, top: tab.offsetTop, width: tab.offsetWidth, height: tab.offsetHeight }, 3305 { type: 'spring', stiffness: 400, damping: 28 } 3306 ); 3307} 3308 3309function updateTabBackgroundIndicator(tabGroup, activeTab) { 3310 const activeBackground = tabGroup.querySelector('.active-background'); 3311 if (!activeBackground || !activeTab) return; 3312 3313 activeBackground.style.opacity = '1'; 3314 3315 if ((activeTab.offsetLeft === 0 || activeTab.offsetWidth === 0)) { 3316 observeUntilVisible(activeTab, () => setBackgroundPosition(activeBackground, activeTab)); 3317 return; 3318 } 3319 3320 setBackgroundPosition(activeBackground, activeTab); 3321} 3322 3323function initTabBackgroundIndicator(tabGroup) { 3324 const tabButtons = tabGroup.querySelectorAll(':scope > .selector-button'); 3325 if (tabButtons.length === 0) return; 3326 3327 const activeBackground = document.createElement('div'); 3328 activeBackground.classList.add('active-background'); 3329 tabGroup.appendChild(activeBackground); 3330 3331 let initialized = false; 3332 3333 function positionBackground(tab, instant = false) { 3334 if (tab.offsetLeft === 0 && !instant) { 3335 observeUntilVisible(tab, () => positionBackground(tab, true)); 3336 return; 3337 } 3338 if (!initialized || instant) { 3339 setBackgroundPosition(activeBackground, tab); 3340 initialized = true; 3341 } else {
3342 springBackgroundPosition(activeBackground, tab); 3343 } 3344 } 3345 3346 let activeTab = tabGroup.querySelector(':scope > .selector-button.active'); 3347 3348 window.addEventListener('resize', () => { 3349 if (activeTab) positionBackground(activeTab, true); 3350 }); 3351 3352 tabButtons.forEach(tab => { 3353 tab.addEventListener('click', () => { 3354 tabButtons.forEach(button => { 3355 button.classList.remove('active'); 3356 button.setAttribute('aria-selected', 'false'); 3357 }); 3358 3359 activeTab = tab; 3360 tab.classList.add('active'); 3361 tab.setAttribute('aria-selected', 'true'); 3362 3363 requestAnimationFrame(() => positionBackground(tab)); 3364 }); 3365 }); 3366 3367 const isDeviceTabs = tabGroup.closest('.device-tabs'); 3368 const shouldChangeDefault = isDeviceTabs && detectOS(); 3369 3370 if (shouldChangeDefault) { 3371 activeBackground.style.opacity = '0'; 3372 } else if (activeTab) { 3373 positionBackground(activeTab); 3374 } 3375} 3376 3377function initTabSelectors() { 3378 const tabContainers = document.querySelectorAll('.selectors-container'); 3379 if (tabContainers.length === 0) return; 3380 3381 tabContainers.forEach((container) => { 3382 const tabList = container.querySelector('.selector-list'); 3383 if (!tabList) return; 3384 3385 const dataId = container.dataset.id; 3386 const panelsContainer = document.querySelector(`.selector-panels[data-id="${dataId}"]`); 3387 3388 if (panelsContainer) { 3389 initTabContentPanels(container, panelsContainer); 3390 } 3391
3392 initTabBackgroundIndicator(tabList); 3393 }); 3394} 3395 3396function detectOS() { 3397 const platform = navigator.platform.toLowerCase(); 3398 3399 if (platform.includes('win')) { 3400 return 3; 3401 } else if (platform.includes('mac')) { 3402 return 2; 3403 } else if (platform.includes('linux')) { 3404 return 1; 3405 } else { 3406 return 0; 3407 } 3408} 3409 3410function changeTabDefault() { 3411 let os = detectOS(); 3412 3413 if (os) { 3414 const osTabButton = document.querySelector(`.device-tabs`); 3415 3416 if (osTabButton) { 3417 setActiveTabByIndex(osTabButton, os - 1); 3418 } 3419 } 3420} 3421</script>
3421 3422
3423<script> 3424 3425let _animate = null; 3426 3427async function getAnimate() { 3428 if (_animate) return _animate; 3429 const { animate } = await import('https://cdn.jsdelivr.net/npm/motion@latest/+esm'); 3430 _animate = animate; 3431 return animate; 3432} 3433 3434async function openModal(id) { 3435 const backdrop = document.getElementById(id); 3436 if (!backdrop) return; 3437 3438 const modal = backdrop.querySelector('.modal'); 3439 backdrop.classList.remove('hidden'); 3440 document.body.classList.add('modal-open'); 3441 3442 const animate = await getAnimate(); 3443 animate(backdrop, { opacity: [0, 1] }, { duration: 0.2, easing: 'ease-out' }); 3444 animate(modal, { opacity: [0, 1], scale: [0.95, 1] }, { duration: 0.25, easing: [0.34, 1.56, 0.64, 1] }); 3445} 3446 3447async function closeModal(backdrop) { 3448 const modal = backdrop.querySelector('.modal'); 3449 const animate = await getAnimate(); 3450 3451 animate(modal, { opacity: 0, scale: 0.95 }, { duration: 0.15, easing: 'ease-in' }); 3452 await animate(backdrop, { opacity: 0 }, { duration: 0.2, easing: 'ease-in' }); 3453 3454 backdrop.classList.add('hidden'); 3455 document.body.classList.remove('modal-open'); 3456} 3457 3458document.addEventListener('DOMContentLoaded', () => { 3459 getAnimate(); 3460 registerModals(); 3461}); 3462 3463function registerModals() { 3464 document.querySelectorAll('[data-modal-target]').forEach(trigger => { 3465 trigger.addEventListener('click', () => { 3466 const targetId = trigger.getAttribute('data-modal-target'); 3467 if (targetId) openModal(targetId); 3468 }); 3469 }); 3470 3471 document.querySelectorAll('.modal-backdrop').forEach(backdrop => { 3472 document.body.appendChild(backdrop); 3473 3474 backdrop.addEventListener('click', (e) => { 3475 const modalBox = backdrop.querySelector('.modal'); 3476 if (!modalBox.contains(e.target) || e.target.classList.contains('modal-close')) { 3477 closeModal(backdrop); 3478 } 3479 }); 3480 }); 3481} 3482 3483</script>
3483 3484
3485<script> 3486 3487document.addEventListener('DOMContentLoaded', () => { 3488 initCodeTabs(); 3489 removeTabFocus(); 3490}); 3491 3492function removeTabFocus() { 3493 const container = document.querySelector('.hero-right'); 3494 3495 if (container) { 3496 container.querySelectorAll('a, button, input, textarea, select, [tabindex]') 3497 .forEach(el => el.setAttribute('tabindex', '-1')); 3498 } 3499} 3500 3501function initCodeTabs() { 3502 const tabs = Array.from(document.querySelectorAll('.code-gallery-tab')).filter(tab => !tab.classList.contains('filler')); 3503 const codeSnippets = document.querySelectorAll('.code-gallery-snippet'); 3504 const codeTips = document.querySelectorAll('.code-gallery-tip'); 3505 const border = document.querySelector('.code-gallery-tab-border'); 3506 const nextButton = document.querySelector('.hero-footer-next'); 3507 3508 if (tabs.length === 0 || !border) return; 3509 3510 let activeIndex = tabs.findIndex(tab => tab.classList.contains('active')); 3511 if (activeIndex === -1) activeIndex = 0; 3512 3513 function updateBorder(tab) { 3514 const tabRect = tab.getBoundingClientRect(); 3515 const parentRect = tab.parentElement.getBoundingClientRect(); 3516 const parentScrollLeft = tab.parentElement.scrollLeft || 0; 3517 3518 border.style.left = `${tabRect.left - parentRect.left + parentScrollLeft}px`; 3519 border.style.width = `${tabRect.width}px`; 3520 } 3521 3522 function setActiveCodeTab(index) {
3523 tabs.forEach((tab, i) => { 3524 const isActive = i === index; 3525 tab.classList.toggle('active', isActive); 3526 tab.setAttribute('aria-selected', isActive ? 'true' : 'false'); 3527 }); 3528 3529 codeSnippets.forEach((snippet, i) => { 3530 snippet.classList.toggle('visible-code', i === index); 3531 snippet.setAttribute('aria-hidden', i !== index); 3532 }); 3533 3534 codeTips.forEach((tip, i) => { 3535 tip.classList.toggle('active', i === index); 3536 tip.setAttribute('aria-hidden', i !== index); 3537 }); 3538 3539 updateBorder(tabs[index]); 3540 activeIndex = index; 3541 } 3542 3543 tabs.forEach((tab, index) => { 3544 tab.setAttribute('role', 'tab'); 3545 tab.setAttribute('aria-selected', index === activeIndex ? 'true' : 'false'); 3546 3547 tab.addEventListener('click', () => { 3548 setActiveCodeTab(index); 3549 }); 3550 }); 3551 3552 // Listen for scroll events on the tab container to update border position 3553 const tabContainer = tabs[0]?.parentElement; 3554 if (tabContainer) { 3555 tabContainer.addEventListener('scroll', () => { 3556 updateBorder(tabs[activeIndex]); 3557 }); 3558 } 3559 3560 if (nextButton) { 3561 nextButton.addEventListener('click', () => {
3562 setActiveCodeTab((activeIndex + 1) % tabs.length); 3563 }); 3564 } 3565 3566 setActiveCodeTab(activeIndex); 3567} 3568 3569function initCodeAnimations() { 3570 const codeSnippets = document.querySelectorAll('.code-gallery-snippet'); 3571 3572 codeSnippets.forEach(snippet => { 3573 const tokens = snippet.querySelectorAll('.token, .inter-text'); 3574 3575 tokens.forEach((token, i) => { 3576 token.style.animationDelay = `${i * 3 + 30}ms`; 3577 }); 3578 }); 3579} 3580</script>
3580 3581 3582<meta name="viewport" content="width=device-width, initial-scale=1"> 3583 <title>About â Lean Lang </title><meta name="description" content="Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code."> 3584 <link rel="icon" href="https://lean-lang.org/static/favicon-light.ico"> 3585 <link rel="apple-touch-icon" href="https://lean-lang.org/static/apple-touch-icon.png"> 3586 <meta name="theme-color" content="#3D6AC9"> 3587 <meta property="og:title" content="Lean Programming Language"> 3588 <meta property="og:type" content="article"> 3589 <meta property="og:image" content="https://lean-lang.org/static/png/banner.png"> 3590 <meta property="og:url" content="https://lean-lang.org"> 3591 <meta property="og:image:alt" content="Lean Programming Language"> 3592 <meta property="og:site_name" content="Lean Language"> 3593 <meta name="twitter:title" content="Lean Programming Language"> 3594 <meta name="twitter:description" content="Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code."> 3595 <meta name="twitter:image" content="https://lean-lang.org/static/png/banner.png"> 3596 <meta name="twitter:image:alt" content="Lean Programming Language"> 3597 <meta name="twitter:creator" content="@leanprover"> 3598 <meta name="twitter:card" content="summary_large_image"> 3599 <link rel="preconnect" href="https://fonts.googleapis.com"> 3600 <link rel="preconnect" href="https://fonts.gstatic.com" crossorigin="anonymous"> 3601 <link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=Fira+Code:[email protected]&
3601family=Open+Sans:ital,wght@0,300..800;1,300..800&family=Oranienbaum&display=swap"> 3602 <style>/* Base Variables */ 3603:root { 3604 --font-primary: 'Open Sans', Arial, sans-serif; 3605 --font-secondary: 'Oranienbaum', serif; 3606 --fs-xs: 0.75rem; 3607 --fs-sm: 0.875rem; 3608 --fs-base: 1rem; 3609 --fs-md: 17px; 3610 --fs-lg: 1.25rem; 3611 --fs-xl: 2rem; 3612 --fs-2xl: 3.3rem; 3613 --space-1: 0.25rem; 3614 --space-2: 0.5rem; 3615 --space-3: 0.75rem; 3616 --space-4: 1rem; 3617 --space-5: 1.25rem; 3618 --space-6: 1.5rem; 3619 --space-8: 2rem; 3620 --space-10: 2.5rem; 3621 --space-12: 3rem; 3622 --space-13: 3.5rem; 3623 --space-14: 4rem; 3624 --space-16: 5rem; 3625 --gap-sm: var(--space-2); 3626 --gap-md: 10px; 3627 --gap-lg: 30px; 3628 --gap-xl: 100px; 3629 --section-padding: var(--space-10); 3630 --section-padding-top: var(--space-16); 3631 --radius-sm: 0.25rem; 3632 --radius-md: 0.5rem; 3633 --radius-lg: 1rem; 3634 --radius-pill: 9999px; 3635 --container-width: 1240px; 3636 --logo-size: 1.25rem; 3637 --logo-footer-size: 60px; 3638 --icon-size: 64px; 3639 --nav-padding-y: var(--space-6); 3640 --nav-padding-x: 10vw; 3641 --nav-height: calc(var(--nav-padding-y) * 2 + 2em); 3642 --transition-fast: 0.2s; 3643 --transition-base: 0.3s; 3644 --transition-slow: 0.6s; 3645 --transition-delay-none: 0s; 3646 --transition-delay-small: 0.05s; 3647 --transition-delay-medium: 0.1s; 3648 --transition-delay-large: 0.15s; 3649 --animation-delay: 10000ms; 3650 --z-below: -1; 3651 --z-normal: 0; 3652 --z-above: 1; 3653 --z-header: 1000; 3654 --color-surface: #fff; 3655 --color-primary: #386EE0; 3656 --color-primary-focus: #1D4ED8; 3657 --color-primary-light: #4a90e2; 3658 --color-secondary: #607D8B; 3659 --color-text: #333; 3660 --color-text-contrast: white; 3661 --color-text-light: #64748b; 3662 --color-muted: #607D8B; 3663 --color-bg: #F9FBFD; 3664 --color-bg-translucent: rgba(249, 251, 253, 0.81); 3665 --color-white: #fff; 3666 --color-border: #E4EBF3; 3667 --color-border-nav: #E4EBF3; 3668 --color-border-light: #D1D9E2; 3669 --color-hover: rgba(56, 110, 224, 0.08); 3670 --color-link-hover: #0073e6; 3671 --color-shadow: rgba(35, 55, 139, 0.1); 3672 --btn-bg: var(--color-primary); 3673 --btn-text: var(--color-white); 3674 --btn-font: var(--font-primary); 3675 --btn-radius: var(--radius-md); 3676 --card-bg: var(--color-white); 3677 --card-border: var(--color-border-light); 3678 --testimonial-bg: var(--color-primary); 3679 --testimonial-text: var(--color-white); 3680} 3681 3682/* Dark Theme */ 3683.dark-theme { 3684 --color-surface: #121212; 3685 --color-primary: #3b94ff; 3686 --color-primary-focus: #669df6; 3687 --color-primary-light: #6aadfe; 3688 --color-secondary: #aabfc9; 3689 --color-text: #eee; 3690 --color-text-light: #bbb; 3691 --color-text-contrast: white; 3692 --color-muted: #90a4ae; 3693 --color-bg: #181818; 3694 --color-bg-translucent: rgba(24, 24, 24, 0.85); 3695 --color-white: #1e1e1e; 3696 --color-border: #333; 3697 --color-border-nav: #333; 3698 --color-border-light: #444; 3699 --color-hover: rgba(255, 255, 255, 0.08); 3700 --color-link-hover: #4d9efc; 3701 --color-shadow: rgba(0, 0, 0, 0.5); 3702 --btn-bg: var(--color-primary); 3703 --btn-text: var(--color-white); 3704 --card-bg: #1f1f1f; 3705 --card-border: #2a2a2a; 3706 --testimonial-bg: #2e3a59; 3707 --testimonial-text: #fff; 3708}</style><link rel="apple-touch-icon" href="apple-touch-icon.png"> 3709
3709<script async="" src="https://plausible.io/js/pa-RTua_4FfKHhfAvAc3liZd.js"></script>
3709 3710
3710<script> 3711 window.plausible=window.plausible||function(){(plausible.q=plausible.q||[]).push(arguments)},plausible.init=plausible.init||function(i){plausible.o=i||{}}; 3712 plausible.init()</script>
3712 3713 </head> 3714 <body> 3715 <noscript><div class="no-js-warning"> 3716 If you want the full website experience, enable JS</div> 3717 </noscript><header class="site-header"> 3718 <nav class="navbar" role="navigation" aria-label="Primary navigation"> 3719 <div class="navbar-container container"> 3720 <a class="nav-logo" href="/"><svg width="70" height="20" viewBox="0 0 486 169" xmlns="http://www.w3.org/2000/svg" stroke="#386EE0" fill="transparent" stroke-width="10"><path d="M206.333 5.67949H105.667M206.333 5.67949L243.25 84.5M206.333 5.67949V84.5M243.25 84.5H317.549M243.25 84.5L279.667 163.321L280.889 163.318L317.549 84.5M206.333 84.5V163.321H5V5M206.333 84.5H105.667M317.549 84.5L353 5.67949M353 5.67949V164M353 5.67949H353.667L480.333 163.454H481V5" stroke-linecap="round" stroke-linejoin="round"></path></svg></a><div class="nav-toggle"> 3721 <input type="checkbox" id="nav-toggle" class="nav-toggle-checkbox"><label for="nav-toggle" class="nav-toggle-label" aria-label="Toggle navigation menu">â°</label></div> 3722 <menu class="desktop-menu"><ul class="desktop-menu-part"> 3723 <li class="nav-item"> 3724 <a href="/install" class="nav-link" aria-label="" target="_self">Install</a></li> 3725 <li class="nav-item"> 3726 <a href="/learn" class="nav-link" aria-label="" target="_self">Learn</a></li> 3727 <li class="nav-item"> 3728 <a href="/community" class="nav-link" aria-label="" target="_self">Community</a></li> 3729 <li class="nav-item"> 3730 <a href="/use-cases" class="nav-link" aria-label="" target="_self">Use Cases</a></li> 3731 <li class="nav-item nav-group"> 3732 <a href="/fro" class="nav-link nav-group-label" aria-label="FRO">FRO</a><ul class="nav-group-items"></ul> 3733 </li> 3734 <li class="nav-item nav-divider" aria-hidden="true"> 3735 <span class="divider"></span></li> 3736 <li class="nav-item"> 3737 <a href="https://live.lean-lang.org/?from=lean" class="nav-link" aria-label="" target="_blank">Playground</a></li> 3738 <li class="nav-item"> 3739 <a href="https://leanprover-community.github.io/" class="nav-link" aria-label="" target="_blank">Mathlib</a></li> 3740 <li class="nav-item"> 3741 <a href="https://www.cslib.io/" class="nav-link" aria-label="" target="_blank">CSLib</a></li> 3742 <li class="nav-item"> 3743 <a href="https://reservoir.lean-lang.org/" class="nav-link" aria-label="" target="_blank">Reservoir</a></li> 3744 </ul> 3745 <ul class="desktop-menu-part"> 3746 <li class="nav-item"> 3747 <button class="nav-link change-theme" aria-label="Change Theme"><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" width="25" height="25"><g data-name="Layer 2"><g data-name="moon"><rect width="24" height="24" opacity="0"></rect><path d="M12.3 22h-.1a10.31 10.31 0 0 1-7.34-3.15 10.46 10.46 0 0 1-.26-14 10.13 10.13 0 0 1 4-2.74 1 1 0 0 1 1.06.22 1 1 0 0 1 .24 1 8.4 8.4 0 0 0 1.94 8.81 8.47 8.47 0 0 0 8.83 1.94 1 1 0 0 1 1.27 1.29A10.16 10.16 0 0 1 19.6 19a10.28 10.28 0 0 1-7.3 3zM7.46 4.92a7.93 7.93 0 0 0-1.37 1.22 8.44 8.44 0 0 0 .2 11.32A8.29 8.29 0 0 0 12.22 20h.08a8.34 8.34 0 0 0 6.78-3.49A10.37 10.37 0 0 1 7.46 4.92z"></path></g></g></svg></button></li> 3748 <li class="nav-item"> 3749 <a href="https://github.com/leanprover/lean4" class="nav-link" aria-label="Github" target="_blank"><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" width="25" height="25"><g data-name="Layer 2"><rect width="24" height="24" opacity="0"></rect><path d="M16.24 22a1 1 0 0 1-1-1v-2.6a2.15 2.15 0 0 0-.54-1.66 1 1 0 0 1 .61-1.67C17.75 14.78 20 14 20 9.77a4 4 0 0 0-.67-2.22 2.75 2.75 0 0 1-.41-2.06 3.71 3.71 0 0 0 0-1.41 7.65 7.65 0 0 0-2.09 1.09 1 1 0 0 1-.84.15 10.15 10.15 0 0 0-5.52 0 1 1 0 0 1-.84-.15 7.4 7.4 0 0 0-2.11-1.09 3.52 3.52 0 0 0 0 1.41 2.84 2.84 0 0 1-.43 2.08 4.07 4.07 0 0 0-.67 2.23c0 3.89 1.88 4.93 4.7 5.29a1 1 0 0 1 .82.66 1 1 0 0 1-.21 1 2.06 2.06 0 0 0-.55 1.56V21a1 1 0 0 1-2 0v-.57a6 6 0 0 1-5.27-2.09 3.9 3.9 0 0 0-1.16-.88 1 1 0 1 1 .5-1.94 4.93 4.93 0 0 1 2 1.36c1 1 2 1.88 3.9 1.52a3.89 3.89 0 0 1 .23-1.58c-2.06-.52-5-2-5-7a6 6 0 0 1 1-3.33.85.85 0 0 0 .13-.62 5.69 5.69 0 0 1 .33-3.21 1 1 0 0 1 .63-.57c.34-.1 1.56-.3 3.87 1.2a12.16 12.16 0 0 1 5.69 0c2.31-1.5 3.53-1.31 3.86-1.2a1 1 0 0 1 .63.57 5.71 5.71 0 0 1 .33 3.22.75.75 0 0 0 .11.57 6 6 0 0 1 1 3.34c0 5.07-2.92 6.54-5 7a4.28 4.28 0 0 1 .22 1.67V21a1 1 0 0 1-.94 1z"></path></g></svg></a></li> 3750 </ul> 3751 </menu></div> 3752 <menu class="mobile-nav"><ul class="nav-list"> 3753 <li class="nav-item"> 3754 <a href="/install" class="nav-link" aria-label="" target="_self">Install</a></li> 3755 <li class="nav-item"> 3756 <a href="/learn" class="nav-link" aria-label="" target="_self">Learn</a></li> 3757 <li class="nav-item"> 3758 <a href="/community" class="nav-link" aria-label="" target="_self">Community</a></li> 3759 <li class="nav-item"> 3760 <a href="/use-cases" class="nav-link" aria-label="" target="_self">Use Cases</a></li> 3761 <li class="nav-item"> 3762 <a href="https://live.lean-lang.org/?from=lean" class="nav-link" aria-label="" target="_blank">Playground</a></li> 3763 <li class="nav-item"> 3764 <a href="https://leanprover-community.github.io/" class="nav-link" aria-label="" target="_blank">Mathlib</a></li> 3765 <li class="nav-item"> 3766 <a href="https://www.cslib.io/" class="nav-link" aria-label="" target="_blank">CSLib</a></li> 3767 <li class="nav-item"> 3768 <a href="https://reservoir.lean-lang.org/" class="nav-link" aria-label="" target="_blank">Reservoir</a></li> 3769 <li class="nav-item has-submenu"> 3770 <input type="checkbox" id="mobile-group-FRO-1710831059350241967" class="mobile-group-toggle" hidden="true"><label for="mobile-group-FRO-1710831059350241967" class="nav-link" aria-label="Toggle FRO navigation menu">FRO</label><ul class="submenu"> 3771 <li class="nav-item"> 3772 <a href="/fro" class="nav-link" aria-label="FRO">Home</a></li> 3773 <li class="nav-item active"> 3774 <a href="/fro/about" class="nav-link" aria-label="" target="_self">About</a></li> 3775 <li class="nav-item"> 3776 <a href="/fro/team" class="nav-link" aria-label="" target="_self">Team</a></li> 3777 <li class="nav-item"> 3778 <a href="/fro/roadmap" class="nav-link" aria-label="" target="_self">Roadmap</a></li> 3779 <li class="nav-item"> 3780 <a href="/fro/contact" class="nav-link" aria-label="" target="_self">Contact</a></li> 3781 </ul> 3782 </li> 3783 </ul> 3784 </menu></nav> 3785 <nav class="sub-navbar"> 3786 <div class="navbar-container container"> 3787 <a class="nav-logo" href="/fro"><svg width="70" height="20" viewBox="-60 0 385 169" fill="transparent" xmlns="http://www.w3.org/2000/svg" stroke="#386EE0" stroke-width="10"><path d="M6.5 5.00001V163.454H5L5.5 87M5.5 87V5.00001L121.5 5M5.5 87L106.5 87M121.5 5V87M121.5 5L170.5 4.99988C213.864 4.99988 232.527 13.4976 232.527 45.9891C232.527 66.3579 224.406 77.297 209.027 82.6298M121.5 166V87M121.5 87L170.5 86.9782C186.2 87.1741 199.12 86.0654 209.027 82.6298M235.027 166L209.027 82.6298" stroke-linejoin="round"></path>
3787<path d="M308 6C347.14 6 379.5 40.3357 379.5 83.5C379.5 126.664 347.14 161 308 161C268.86 161 236.5 126.664 236.5 83.5C236.5 40.3357 268.86 6 308 6Z"></path></svg></a><ul class="nav-list"> 3788 <li class="nav-item"> 3789 <a href="/fro" class="nav-link" aria-label="" target="_self">Home</a></li> 3790 <li class="nav-item active"> 3791 <a href="/fro/about" class="nav-link" aria-label="" target="_self">About</a></li> 3792 <li class="nav-item"> 3793 <a href="/fro/team" class="nav-link" aria-label="" target="_self">Team</a></li> 3794 <li class="nav-item"> 3795 <a href="/fro/roadmap" class="nav-link" aria-label="" target="_self">Roadmap</a></li> 3796 <li class="nav-item"> 3797 <a href="/fro/contact" class="nav-link" aria-label="" target="_self">Contact</a></li> 3798 </ul> 3799 </div> 3800 </nav> 3801 </header> 3802 <main class="container fro"><div class="post-center post-page"> 3803 <article class="post-container"><div class="post-content"> 3804 <h1 class="page-title"> 3805 About</h1> 3806 <section> 3807 <h2 id="the-lean-fro"> 3808 The Lean FRO<span class="permalink-widget inline"><a href="fro/about/#the-lean-fro" title="Permalink">ð</a></span></h2> 3809 <p> 3810 <strong>The Lean Focused Research Organization works to make formal verification more accessible across mathematics research, software and hardware verification, and AI-assisted theorem proving.</strong> Since its formation in July 2023 as a non-profit organization under Convergent Research, the FRO pursues a focused mission to improve Lean's critical systems through enhanced scalability, usability, documentation, and proof automation while guiding Lean toward long-term self-sustainability.</p> 3811 <p> 3812 The Lean FRO is led by Chief Architect and co-founder <a href="https://leodemoura.github.io/blog/">Leonardo de Moura</a>, currently a senior principal applied scientist in the Automated Reasoning Group at Amazon Web Services. De Moura created Lean in 2013 and previously worked on automated reasoning and theorem proving at Microsoft Research and SRI International.</p> 3813 <p> 3814 Working alongside de Moura is Head of Engineering and co-founder Sebastian Ullrich and a <a href="/fro/team">team of skilled researchers and engineers</a> with specialized expertise across diverse aspects of Lean development. The Lean FRO team is globally diverse and many team members are recruited directly from the very active Lean community. The team actively engages with the community to promote Lean adoption across academic and industry contexts.</p> 3815 <p> 3816 The Lean FRO gratefully acknowledges support from its funders and supporters, including Alex Gerko, Alfred P. Sloan Foundation, Richard Merkin Foundation, Simons Foundation International, and Convergent Research.</p> 3817 </section> 3818 <section> 3819 <h2 id="a-brief-history-of-lean"> 3820 A Brief History of Lean<span class="permalink-widget inline"><a href="fro/about/#a-brief-history-of-lean" title="Permalink">ð</a></span></h2> 3821 <ul> 3822 <li> 3823 <p> 3824 <strong>September 2026</strong> - Anthropic <a href="https://www.anthropic.com/research/formalizing-fermats-last-theorem">announces</a> Lean formalization of Fermat's Last Theorem; 3825OpenAI's <a href="https://openai.com/index/gpt-6-astra/">GPT-6 Astra</a> helped establish a stronger prime gap bound of 186, with <a href="https://github.com/openai/PrimeGaps186">Lean formalization</a></p> 3826 </li> 3827 <li> 3828 <p> 3829 <strong>August 2026</strong> - OpenAI provides <a href="https://github.com/openai/ten-proofs">Lean certificates</a> and <a href="https://openai.com/index/ten-advances-in-mathematics/">announces progress</a> on 10 research-level mathematical problems; Anthropic <a href="https://www.anthropic.com/research/riemann-zeta">announces new results</a> related to the Riemann zeta function and provides <a href="https://github.com/anthropics/zeta-23-lean">Lean formalizations</a>
3829 that pass Comparator validation; Lean FRO publishes <a href="https://lean-lang.org/fro/roadmap/y4-1/">Year 4 Part 1 Roadmap</a>; <a href="https://www.ibtimes.com/chris-hsu-how-one-programming-language-rewrote-mathematics-why-software-next-3806974">International Business Times</a> interviews Chris Hsu: 'How One Programming Language Rewrote Mathematics and Why Software Is Next'; Kim Morrison launches <a href="https://palomar-registry.org/">Palomar</a>, a Registry of Lean-Verified Mathematics</p> 3830 </li> 3831 <li> 3832 <p> 3833 <strong>July 2026</strong> - Amazon Automated reasoning <a href="https://www.amazon.science/news/amazon-is-investing-in-the-lean-focused-research-organization">announces the single largest donation</a> to Lean FRO in the FRO's history; <a href="https://www.microsoft.com/en-us/research/blog/verifying-rust-cryptography-in-symcrypt-from-standards-to-code/">Microsoft Research</a> reports on how Lean, via the Aeneas toolchain, formally verifies production cryptographic algorithms in SymCrypt; <a href="https://www.newscientist.com/article/2533518-mathematicians-put-ai-to-work-on-fermats-last-theorem/">New Scientist</a> reports on AI use supporting the Lean formalization of Fermat's Last Theorem; <a href="https://kim-em.github.io/hex-dev/">the Hex project</a>, a library for computational algebra, is released; a <a href="https://lean-lang.org/eval/problems/erdos_unit_distance_conjecture_false/">1.2M line human-in-the-loop proof</a> of the falsity of the Erdos unit-distance problem is submitted to Lean Eval; <a href="https://taucetiproject.github.io/TauCeti/">Tau Ceti</a> launched, AI-authored Lean mathematics downstream of Mathlib, with human-owned roadmaps and AI adversarial review against open rubrics; <a href="https://github.com/BobDyLean/dylean">Bob DyLean</a>, a framework for the symbolic analysis of cryptographic protocols, is open-sourced; Google DeepMind <a href="https://deepmind.google/public-policy/conjecture-machines-ai-agents-and-the-new-validation-bottleneck-in-science/">publishes on AI conjecture machines</a> and Lean as the validation layer for AI-generated science</p> 3834 </li> 3835 <li> 3836 <p> 3837 <strong>June 2026</strong> - Quanta Books publishes <a href="https://www.quantabooks.org/books/the-proof-in-the-code/">The Proof in the Code</a>, "the definitive account of the birth and rise of Lean"; Lean is featured as part of Simons Foundation <a href="https://www.simonsfoundation.org/2026/06/23/from-trust-to-verification-leans-impact-on-mathematics/">2025 Annual Report</a>; <a href="https://fortune.com/2026/06/01/axiom-math-econlib-antitrust-economic-theory-verified/">Fortune magazine</a> announces Axiom's EconLib, formalizing economic theory in Lean; <a href="https://comparator.live.lean-lang.org">Comparator</a>, a sandboxed judge for Lean proofs that exports and re-checks independently, is launched; <a href="https://lean-lang.org/eval/">Lean Eval</a>, a public submission-based leaderboard of hard formalization problems, is launched; <a href='https://stat-lib.github.io/'>StatLib</a>, a library for mathematical statistics, is launched; <a href="https://pramaanalabs.ai/blog/we-raised-27m-to-build-a-compiler-for-mission-critical-ai">Pramaana Labs</a> launches out of stealth with <a href="https://techcrunch.com/2026/06/17/pramaana-labs-raises-27-million-seed-round-from-khosla-ventures-to-bring-formal-verification-to-ai/">$27M from Khosla Ventures</a> for Lean-based formal verification</p> 3838 </li> 3839 <li> 3840 <p> 3841 <strong>May 2026</strong> - Google DeepMind announces <a href="https://arxiv.org/abs/2605.22763v1">AlphaProof Nexus</a> and autonomous proofs of <a href="https://github.com/google-deepmind/alphaproof-nexus-results">9 ErdÅs problems</a>; SAIR convenes the <a href="https://sair.foundation/events/science-ai-summit-2026">Science x AI Summit</a> in Palo Alto, foregrounding Lean and AI-assisted proof discovery; NASA holds its <a href="https://nfm2026.github.io/">Formal Methods Symposium</a> with <a href="https://nfm2026.github.io/keynote_speakers/">keynotes</a> on <a href="https://lean-lang.org">Lean</a>, <a href="https://www.cslib.io/">CSLib</a> and <a href="https://aristotle.harmonic.fun/">Aristotle</a>; <a href="https://lean-dojo.github.io/TorchLean/">TorchLean</a> is released, bridging PyTorch and Lean</p> 3842 </li> 3843 <li> 3844 <p> 3845 <strong>April 2026</strong> - OpenAI <a href="https://openai.com/index/introducing-gpt-5-5/">releases ChatGPT 5.5</a>, used internally by OpenAI to discover a new Lean-verified proof relating to off-diagonal Ramsey numbers; <a href="https://www.economist.com/science-and-technology/2026/04/08/ai-models-could-offer-mathematicians-a-common-language">The Economist</a> profiles Lean-powered AI math startups; <a href="https://beneficial-ai-foundation.github.io/SVIL2026/">Software Verification in Lean</a> takes place in Paris; The <a href="https://www.beneficialaifoundation.org/signal-shot">Signal Shot</a> challenge is announced;
3845 The <a href="https://competition.sair.foundation/competitions/mathematics-distillation-challenge-equational-theories-stage2/overview">SAIR Mathematics Distillation Challenge Stage 2</a> announced; <a href="https://www.newscientist.com/article/2522687-the-secret-project-to-settle-controversial-maths-proof-with-a-computer/">New Scientist</a> reports on the LANA project; <a href="https://arena.lean-lang.org">Lean Kernel Arena</a>, a public benchmarking of independent proof checkers, goes live</p> 3846 </li> 3847 <li> 3848 <p> 3849 <strong>March 2026</strong> - <a href="https://spectrum.ieee.org/scenario-modeling-and-array-design-for-non-terrestrial-networks-ntns">IEEE Spectrum</a> reports on formalization in Lean of proof of sphere packing in 24-dimensions via Math, Inc.'s Gauss; The <a href="https://zen.ac.jp/en/zmc/topics/jwz-o8xr3v6f">LANA Project</a> is announced; The <a href="https://competition.sair.foundation/competitions/mathematics-distillation-challenge-equational-theories-stage1/overview">SAIR Mathematics Distillation Challenge Stage 1</a> announced; The <a href="https://github.com/leanprover/lean4">Lean GitHub repository</a> is starred over 7,500 times; <a href=" https://mistral.ai/news/leanstral">Leanstral</a>, the first open-source code agent designed for Lean 4, released</p> 3850 </li> 3851 <li> 3852 <p> 3853 <strong>February 2026</strong> - <a href="https://www.wired.com/story/a-new-ai-math-ai-startup-just-cracked-4-previously-unsolved-problems/">Wired reports</a> on how Lean enables Axiom's proof of Fel's Conjecture; <a href="https://cacm.acm.org/news/math-in-the-age-of-ai/">Communications of the ACM</a> reports on Lean's critical role in verifying AI mathematical output; <a href="https://harmonic.fun/news/lean-fro-donation/">Harmonic announces</a> inaugural donation to Lean FRO to advance formal reasoning and mathematical AI</p> 3854 </li> 3855 <li> 3856 <p> 3857 <strong>January 2026</strong> - Advances in <a href="https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems">human-AI collaborative proof development</a> yields proofs and Lean formalizations to previously open ErdÅs problems, <a href="https://www.newscientist.com/article/2511954-amateur-mathematicians-solve-long-standing-maths-problems-with-ai/">New Scientist</a> highlights Lean's key role in powering Harmonic's Aristotle; AxiomProver <a href="https://github.com/AxiomMath/putnam2025">solves 8 of 12 Putnam problems</a> during the Putnam competition</p> 3858 </li> 3859 <li> 3860 <p> 3861 <strong>December 2025</strong> - The Lean@Google Hackathon takes place, initiating development of the <strong>SymM</strong> framework, a lightweight monadic framework for high-performance software verification; The <a href="https://arxiv.org/abs/2512.07087">Equational Theories Project</a> is completed</p> 3862 </li> 3863 <li> 3864 <p> 3865 <strong>November 2025</strong> - <a href="https://www.nature.com/articles/s41586-025-09833-y">Nature</a> publishes a paper by Google DeepMind on their silver medal performance at the 2024 IMO; Lean profiled in <a href="https://venturebeat.com/ai/lean4-how-the-theorem-prover-works-and-why-its-the-new-competitive-edge-in/">VentureBeat</a> and <a href="https://www.newscientist.com/article/2503500-the-biggest-controversy-in-maths-could-be-settled-by-a-computer/">New Scientist</a></p> 3866 </li> 3867 <li> 3868 <p> 3869 <strong>October 2025</strong> - Harmonic releases <a href="https://aristotle.harmonic.fun/">Aristotle</a>, a mathematical superintelligence with Lean API; <a href="https://axiommath.ai/">Axiom</a> launches, with the goal of building a quantitative super-intelligence; <a href="https://verse-lab.github.io/papers/loom-preprint.pdf">Velvet</a> is released, a verifier for imperative programs in Lean; ErdÅs 707 is resolved with a <a href="https://arxiv.org/abs/2510.19804">vibe-coded Lean proof</a></p> 3870 </li> 3871 <li> 3872 <p> 3873 <strong>September 2025</strong>
3873 - Official launch of the <a href="https://mathlib-initiative.org/">Mathlib Initiative</a>; The Lean <a href="https://marketplace.visualstudio.com/items?itemName=leanprover.lean4&ssr=false#overview">VS Code development environment</a> is installed over 100,000 times</p> 3874 </li> 3875 <li> 3876 <p> 3877 <strong>August 2025</strong> - Lean FRO begins 3rd year of operations and ships the <a href="https://lean-lang.org/doc/reference/latest/releases/v4.22.0/#release-v4___22___0"><strong>grind</strong> tactic and new compiler</a>; <a href="https://www.cslib.io/">CSLib</a> project, a foundation for Computer Science in Lean, announced; The <a href="https://florisvandoorn.com/carleson/">Carleson project</a> is completed; <a href="https://google-deepmind.github.io/formal-conjectures/">DeepMind Formal Conjectures</a> project, cataloguing formalised statements of open mathematical conjectures in Lean 4, is established</p> 3878 </li> 3879 <li> 3880 <p> 3881 <strong>July 2025</strong> - <a href="https://www.renaissancephilanthropy.org/news-and-insights/lean-fro-and-mathlib-receive-10m-from-xtx-markets-founder-alex-gerko-to-further-advance-the-use-of-ai-for-mathematical-research">$10MM in new funding from Alex Gerko is announced</a>. $5MM supports a new Mathlib Initiative and $5MM is awarded to Lean FRO to support development of new Lean features; Lean is awarded the <a href="https://cadeinc.org/Skolem-Award">2025 Skolem Award</a> for 2015 CADE paper "The Lean Theorem Prover (System Description)"; Aristotle (Harmonic) <a href="https://www.harmonic.fun/news/imo-gold">wins IMO gold</a> using Lean; ByteDance's Seed Prover <a href="https://seed.bytedance.com/en/blog/bytedance-seed-prover-achieves-silver-medal-score-in-imo-2025">wins IMO silver</a> using Lean; <a href="https://lean-lang.org/use-cases/veil/">Veil</a> is presented at CAV25</p> 3882 </li> 3883 <li> 3884 <p> 3885 <strong>June 2025</strong> - Lean is awarded the <a href="https://www.sigplan.org/Awards/Software/#2025_Lean_Theorem_Prover">2025 ACM SIGPLAN Programming Languages Software Award</a>; SampCert, an open-source Lean library of verified differential-privacy primitives deployed in AWS Clean Rooms <a href="https://dl.acm.org/doi/10.1145/3729294">presented at PLDI 2025</a></p> 3886 </li> 3887 <li> 3888 <p> 3889 <strong>May 2025</strong> - Over <a href="https://leanprover-community.github.io/teaching/courses.html">50 university-level courses</a> have been taught using Lean</p> 3890 </li> 3891 <li> 3892 <p> 3893 <strong>February 2025</strong> - The <a href="https://github.com/leanprover/lean4">Lean GitHub repository</a> is starred over 5,000 times</p> 3894 </li> 3895 <li> 3896 <p> 3897 <strong>January 2025</strong> - The <a href="https://github.com/leanprover-community/mathlib4">Mathlib4 GitHub repository</a> exceeds 20,000 contributions</p> 3898 </li> 3899 <li> 3900 <p> 3901 <strong>December 2024</strong> - Over 30,000 installs of the Lean <a href="https://marketplace.visualstudio.com/items?itemName=leanprover.lean4">VS Code development environment</a> occur in a single calendar year</p> 3902 </li> 3903 <li> 3904 <p> 3905 <strong>November 2024</strong> - <a href="https://github.com/lean-dojo/LeanCopilot">Lean Copilot</a> is covered by Scientific American in <a href="https://www.scientificamerican.com/article/mathematicians-newest-assistants-are-artificially-intelligent/">Mathematicians' Newest Assistants Are Artificially Intelligent</a></p> 3906 </li> 3907 <li> 3908 <p> 3909 <strong>September 2024</strong> - The <a href="https://teorth.github.io/equational_theories/">Equational Theories project</a> is established; <a href="https://github.com/PatrickMassot/verbose-lean4">Lean Verbose</a>, a framework of controlled natural language tactics and commands, presented at ITP 2024; The <a href="https://leanprover.zulipchat.com/">Lean Community Zulip channel</a> grows to over 10,000 members</p> 3910 </li> 3911 <li> 3912 <p> 3913 <strong>July 2024</strong> - AlphaProof achieves <a href="https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/">IMO silver medal performance</a> using Lean and Mathlib. The New York Times covers it in <a href="https://www.nytimes.c
3913om/2024/07/25/science/ai-math-alphaproof-deepmind.html">Move Over, Mathematicians, Here Comes AlphaProof</a>, Nature in <a href="https://www.nature.com/articles/d41586-024-02441-2">DeepMind hits milestone in solving maths problems â AI's next grand challenge</a>, MIT Technology Review in <a href="https://www.technologyreview.com/2024/07/25/1095315/google-deepminds-ai-systems-can-now-solve-complex-math-problems/">Google DeepMind's new AI systems can now solve complex math problems</a>, and Fortune in <a href="https://fortune.com/2024/07/25/google-researchers-claim-new-breakthrough-in-getting-ai-to-solve-tough-high-school-math-problems/">Google researchers claim new breakthrough in getting AI to solve tough high school math problems</a></p> 3914 </li> 3915 <li> 3916 <p> 3917 <strong>June 2024</strong> - <a href="https://harmonic.fun/">Harmonic</a> launches, the first startup based on Lean. The New York Times covers it in <a href="https://www.nytimes.com/2024/09/23/technology/ai-chatbots-chatgpt-math.html">Is Math the Path to Chatbots That Don't Make Stuff Up?</a> and Sequoia Capital in <a href="https://www.sequoiacap.com/podcast/training-data-harmonic/">Training Data: Ep14</a>; Scientific American publishes <a href="https://www.scientificamerican.com/article/ai-will-become-mathematicians-co-pilot/">AI Will Become Mathematicians' 'Co-Pilot'</a>; The <a href="https://florisvandoorn.com/carleson/">Carleson project</a> is established</p> 3918 </li> 3919 <li> 3920 <p> 3921 <strong>April 2024</strong> - <a href="https://aws.amazon.com/blogs/opensource/lean-into-verified-software-development/">Lean verification of AWS Cedar policies</a> is released</p> 3922 </li> 3923 <li> 3924 <p> 3925 <strong>January 2024</strong> - First public launch of <a href="https://github.com/leanprover/verso">Verso</a>, the Lean authoring tool</p> 3926 </li> 3927 <li> 3928 <p> 3929 <strong>December 2023</strong> - The <a href="https://imperialcollegelondon.github.io/FLT/">Fermat's Last Theorem project</a> is established</p> 3930 </li> 3931 <li> 3932 <p> 3933 <strong>November 2023</strong> - The <a href="https://teorth.github.io/pfr/">Polynomial Freiman-Ruzsa conjecture project</a> is established. Quanta Magazine covers it in <a href="https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/">'A-Team' of Math Proves a Critical Link Between Addition and Sets</a></p> 3934 </li> 3935 <li> 3936 <p> 3937 <strong>October 2023</strong> - Quanta Magazine publishes <a href="https://www.quantamagazine.org/the-deep-link-equating-math-proofs-and-computer-programs-20231011/">The Deep Link Equating Math Proofs and Computer Programs</a></p> 3938 </li> 3939 <li> 3940 <p> 3941 <strong>September 2023</strong> - Lean 4.0 is officially released</p> 3942 </li> 3943 <li> 3944 <p> 3945 <strong>July 2023</strong> - <a href="https://lean-lang.org/fro/">Lean FRO</a> is founded by <a href="https://leodemoura.github.io/">Leonardo de Moura</a> and <a href="https://sebasti.a.nullri.ch/">Sebastian Ullrich</a>; The New York Times publishes <a href="https://www.nytimes.com/2023/07/02/science/ai-mathematics-machine-learning.html">A.I. Is Coming for Mathematics, Too</a>; The Lean community completes the port of <a href="https://github.com/leanprover-community/mathlib4">Mathlib</a> from Lean 3 to Lean 4; <a href="https://leandojo.org/">LeanDojo</a> is presented at NeurIPS 2023</p> 3946 </li> 3947 <li> 3948 <p> 3949 <strong>February 2023</strong> - Nature publishes <a href="https://www.nature.com/articles/d41586-023-00487-2">How will AI change mathematics? Rise of chatbots highlights discussion</a></p> 3950 </li> 3951 <li> 3952 <p> 3953 <strong>August 2022</strong> - The <a href="https://github.com/AeneasVerif/aeneas">Aeneas verification toolchain</a> is presented at ICFP 2022; Development begins on <a href="https://github.com/leanprover-community/iris-lean">Iris-Lean</a>, a higher-order concurrent separation logic framework</p> 3954 </li> 3955 <li> 3956 <p> 3957 <strong>November 2021</strong> - The Lean Community Zulip channel grows to over 5,000 members</p> 3958 </li> 3959 <li> 3960 <p> 3961 <strong>September 2021</strong> - The Lean GitHub repository is starred over 1,000 times</p> 3962 </li> 3963 <li> 3964 <p> 3965 <strong>August 2021</strong> - The Mathlib3 GitHub repository exceeds 10,000 contributions</p> 3966 </li> 3967 <li> 3968 <p> 3969 <strong>July 2021</strong> - The <a href="https://github.com/leanprover-community/lean-liquid">Liquid Tensor Experiment project</a> is completed. Nature covers it in <a href="https://www.nature.com/articles/d41586-021-01627-2">Mathematicians welcome computer-assisted proof in 'grand unification' theory</a> and Quanta Magazine in <a href="https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/">Proof Assistant Makes Jump to Big-League Math</a></p> 3970 </li> 3971 <li> 3972 <p> 3973 <strong>May 2021</strong> - The Mathlib4 GitHub repository is created</p> 3974 </li> 3975 <li> 3976 <p> 3977 <strong>December 2020</strong> - The Liquid Tensor Experiment project is established</p> 3978 </li> 3979 <li> 3980 <p> 3981 <strong>October 2020</strong> - Quanta Magazine publishes <a href="https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/">Building the Mathematical Library of the Future</a></p> 3982 </li> 3983 <li> 3984 <p> 3985 <strong>October 2019</strong> - The <a href="https://adam.math.hhu.de/#/g/leanprover-community/nng4">Natural Number Game</a> v1.0 is released</p> 3986 </li> 3987 <li> 3988 <p> 3989 <strong>January 2019</strong> - The first <a href="https://lean-forward.github.io/lean-together/2019/">Lean Together workshop</a> is hosted at Vrije Universiteit Amsterdam</p> 3990 </li> 3991 <li> 3992 <p> 3993 <strong>April 2018</strong> - Lean 4 development begins</p> 3994 </li> 3995 <li> 3996 <p> 3997 <strong>February 2018</strong> - The Lean Community Zulip channel is established</p> 3998 </li> 3999 <li> 4000 <p> 4001 <strong>July 2017</strong> - The Mathlib3 mathematical library is created</p> 4002 </li> 4003 <li> 4004 <p> 4005 <strong>June 2017</strong>
4005 - The <a href="https://www.newton.ac.uk/event/bpr/">Big Proof Programme</a>, focused on bringing proof technology into mainstream mathematical practice, takes place at Isaac Newton Institute for Mathematical Sciences</p> 4006 </li> 4007 <li> 4008 <p> 4009 <strong>January 2017</strong> - Lean 3.0 is officially released</p> 4010 </li> 4011 <li> 4012 <p> 4013 <strong>August 2015</strong> - "The Lean Theorem Prover (System Description)" is published at CADE-25</p> 4014 </li> 4015 <li> 4016 <p> 4017 <strong>January 2015</strong> - The first university course using Lean, <a href="https://leanprover.github.io/cmu-15815-s15/index.html">15â815 Interactive Theorem Proving</a>, is taught at Carnegie Mellon University</p> 4018 </li> 4019 <li> 4020 <p> 4021 <strong>June 2014</strong> - Official release of Lean 0.1</p> 4022 </li> 4023 <li> 4024 <p> 4025 <strong>July 2013</strong> - First commit to the Lean repository 4026</p> 4027 </li> 4028 </ul> 4029 </section> 4030 </div> 4031 </article></div> 4032 </main><footer role="contentinfo" aria-label="Site footer"><div class="footer-grid container"> 4033 <nav class="footer-column" aria-label="LEAN"> 4034 <a href="/"><svg width="80" height="40" viewBox="0 0 486 169" xmlns="http://www.w3.org/2000/svg" stroke="white" fill="transparent" stroke-width="10"><path d="M206.333 5.67949H105.667M206.333 5.67949L243.25 84.5M206.333 5.67949V84.5M243.25 84.5H317.549M243.25 84.5L279.667 163.321L280.889 163.318L317.549 84.5M206.333 84.5V163.321H5V5M206.333 84.5H105.667M317.549 84.5L353 5.67949M353 5.67949V164M353 5.67949H353.667L480.333 163.454H481V5" stroke-linecap="round" stroke-linejoin="round"></path></svg></a></nav> 4035 <nav class="footer-column" aria-label="LEAN"> 4036 <h3 id="get-started" class="footer-heading"> 4037 Get Started</h3> 4038 <ul class="footer-links"> 4039 <li> 4040 <a href="/install" class="footer-text" target="_self">Install</a></li> 4041 <li> 4042 <a href="/learn" class="footer-text" target="_self">Learn</a></li> 4043 <li> 4044 <a href="/community" class="footer-text" target="_self">Community</a></li> 4045 <li> 4046 <a href="https://live.lean-lang.org/?from=lean" class="footer-text" target="_blank">Playground</a></li> 4047 <li> 4048 <a href="https://reservoir.lean-lang.org/" class="footer-text" target="_blank">Reservoir</a></li> 4049 </ul> 4050 </nav> 4051 <nav class="footer-column" aria-label="Documentation"> 4052 <h3 id="documentation" class="footer-heading"> 4053 Documentation</h3> 4054 <ul class="footer-links"> 4055 <li> 4056 <a href="/doc/reference/latest/" class="footer-text" target="_self">Language reference</a></li> 4057 <li> 4058 <a href="/doc/api/" class="footer-text" target="_self">Lean API</a></li> 4059 <li> 4060 <a href="/use-cases" class="footer-text" target="_self">Use cases</a></li> 4061 <li> 4062 <a href="/faq" class="footer-text" target="_self">FAQ</a></li> 4063 <li> 4064 <a href="/learn#how-to-cite-lean" class="footer-text" target="_self">Cite Lean</a></li> 4065 </ul> 4066 </nav> 4067 <nav class="footer-column" aria-label="Resources"> 4068 <h3 id="resources" class="footer-heading"> 4069 Resources</h3> 4070 <ul class="footer-links"> 4071 <li> 4072 <a href="https://marketplace.visualstudio.com/items?itemName=leanprover.lean4" class="footer-text" target="_blank">VS Code extension</a></li> 4073 <li> 4074 <a href="https://loogle.lean-lang.org/" class="footer-text" target="_blank">Loogle!</a></li> 4075 <li> 4076 <a href="https://verso.lean-lang.org/" class="footer-text" target="_blank">Verso</a></li> 4077 <li> 4078 <a href="https://leanprover-community.github.io/" class="footer-text" target="_blank">Mathlib</a></li> 4079 <li> 4080 <a href="https://www.cslib.io/" class="footer-text" target="_blank">CSLib</a></li> 4081 </ul> 4082 </nav> 4083 <nav class="footer-column" aria-label="FRO"> 4084 <h3 id="fro" class="footer-heading"> 4085 FRO</h3> 4086 <ul class="footer-links"> 4087 <li> 4088 <a href="/fro" class="footer-text" target="_self">Vision</a></li> 4089 <li> 4090 <a href="/fro/team" class="footer-text" target="_self">Team</a></li> 4091 <li> 4092 <a href="/fro/roadmap/y4-1" class="footer-text" target="_self">Roadmap</a></li> 4093 <li> 4094 <a href="https://leodemoura.github.io/blog/" class="footer-text" target="_blank">Founder's Blog</a></li> 4095 </ul> 4096 </nav> 4097 <nav class="footer-column" aria-label="Policies"> 4098 <h3 id="policies" class="footer-heading"> 4099 Policies</h3> 4100 <ul class="footer-links"> 4101 <li> 4102 <a href="/privacy" class="footer-text" target="_self">Privacy Policy</a></li> 4103 <li> 4104 <a href="/terms" class="footer-text" target="_self">Terms of Use</a></li> 4105 <li> 4106 <a href="/trademark-policy" class="footer-text" target="_self">Lean Trademark Policy</a></li> 4107 </ul> 4108 </nav> 4109 </div> 4110 <div class="footer-divider container" role="separator"></div> 4111 <div class="footer-bottom container"> 4112 <div class="footer-copy"> 4113 © 2026 Lean FRO. All rights reserved.</div> 4114 <div class="footer-socials"> 4115 <label class="theme-switch"><input type="checkbox" class="change-theme"><div class="switch-container">
4116 <span class="slider"></span></div> 4117 </label><a href="https://bsky.app/profile/lean-lang.org" aria-label="Bluesky"><svg width="20" height="20" viewBox="0 0 568 501" fill="none" xmlns="http://www.w3.org/2000/svg"><path d="M123.121 33.6637C188.241 82.5526 258.281 181.681 284 234.873C309.719 181.681 379.759 82.5526 444.879 33.6637C491.866 -1.61183 568 -28.9064 568 57.9464C568 75.2916 558.055 203.659 552.222 224.501C531.947 296.954 458.067 315.434 392.347 304.249C507.222 323.8 536.444 388.56 473.333 453.32C353.473 576.312 301.061 422.461 287.631 383.039C285.169 375.812 284.017 372.431 284 375.306C283.983 372.431 282.831 375.812 280.369 383.039C266.939 422.461 214.527 576.312 94.6667 453.32C31.5556 388.56 60.7778 323.8 175.653 304.249C109.933 315.434 36.0535 296.954 15.7778 224.501C9.94525 203.659 0 75.2916 0 57.9464C0 -28.9064 76.1345 -1.61183 123.121 33.6637Z" fill="white"></path></svg></a><a href="https://www.linkedin.com/company/lean-fro" aria-label="LinkedIn"><img width="20" src="../../static/svg/linkedin-white.png" alt="LinkedIn"></a><a href="https://functional.cafe/@leanprover" aria-label="Mastodon"><svg width="20" height="20" viewBox="0 0 74 79" fill="white" xmlns="http://www.w3.org/2000/svg"><path d="M73.7014 17.9592C72.5616 9.62034 65.1774 3.04876 56.424 1.77536C54.9472 1.56019 49.3517 0.7771 36.3901 0.7771H36.2933C23.3281 0.7771 20.5465 1.56019 19.0697 1.77536C10.56 3.01348 2.78877 8.91838 0.903306 17.356C-0.00357857 21.5113 -0.100361 26.1181 0.068112 30.3439C0.308275 36.404 0.354874 42.4535 0.91406 48.489C1.30064 52.498 1.97502 56.4751 2.93215 60.3905C4.72441 67.6217 11.9795 73.6395 19.0876 76.0945C26.6979 78.6548 34.8821 79.0799 42.724 77.3221C43.5866 77.1245 44.4398 76.8953 45.2833 76.6342C47.1867 76.0381 49.4199 75.3714 51.0616 74.2003C51.0841 74.1839 51.1026 74.1627 51.1156 74.1382C51.1286 74.1138 51.1359 74.0868 51.1368 74.0592V68.2108C51.1364 68.185 51.1302 68.1596 51.1185 68.1365C51.1069 68.1134 51.0902 68.0932 51.0695 68.0773C51.0489 68.0614 51.0249 68.0503 50.9994 68.0447C50.9738 68.0391 50.9473 68.0392 50.9218 68.045C45.8976 69.226 40.7491 69.818 35.5836 69.8087C26.694 69.8087 24.3031 65.6569 23.6184 63.9285C23.0681 62.4347 22.7186 60.8764 22.5789 59.2934C22.5775 59.2669 22.5825 59.2403 22.5934 59.216C22.6043 59.1916 22.621 59.1702 22.6419 59.1533C22.6629 59.1365 22.6876 59.1248 22.714 59.1191C22.7404 59.1134 22.7678 59.1139 22.794 59.1206C27.7345 60.2936 32.799 60.8856 37.8813 60.8843C39.1036 60.8843 40.3223 60.8843 41.5447 60.8526C46.6562 60.7115 52.0437 60.454 57.0728 59.4874C57.1983 59.4628 57.3237 59.4416 57.4313 59.4098C65.3638 57.9107 72.9128 53.2051 73.6799 41.2895C73.7086 40.8204 73.7803 36.3758 73.7803 35.889C73.7839 34.2347 74.3216 24.1533 73.7014 17.9592ZM61.4925 47.6918H53.1514V27.5855C53.1514 23.3526 51.3591 21.1938 47.7136 21.1938C43.7061 21.1938 41.6988 23.7476 41.6988 28.7919V39.7974H33.4078V28.7919C33.4078 23.7476 31.3969 21.1938 27.3894 21.1938C23.7654 21.1938 21.9552 23.3526 21.9516 27.5855V47.6918H13.6176V26.9752C13.6176 22.7423 14.7157 19.3795 16.9118 16.8868C19.1772 14.4 22.1488 13.1231 25.8373 13.1231C30.1064 13.1231 33.3325 14.7386 35.4832 17.9662L37.5587 21.3949L39.6377 17.9662C41.7884 14.7386 45.0145 13.1231 49.2765 13.1231C52.9614 13.1231 55.9329 14.4 58.2055 16.8868C60.4017 19.3772 61.4997 22.74 61.4997 26.9752L61.4925 47.6918Z" fill="inherit"></path></svg></a><a href="https://x.com/leanprover" aria-label="X (Twitter)"><svg width="20" height="20" viewBox="0 0 1200 1227" fill="none" xmlns="http://www.w3.org/2000/svg"><path d="M714.163 519.284L1160.89 0H1055.03L667.137 450.887L357.328 0H0L468.492 681.821L0 1226.37H105.866L515.491 750.218L842.672 1226.37H1200L714.137 519.284H714.163ZM569.165 687.828L521.697 619.934L144.011 79.6944H306.615L611.412 515.685L658.88 583.579L1055.08 1150.3H892.476L569.165 687.854V687.828Z" fill="white"></path></svg></a><a href="https://leanprover.zulipchat.com/" aria-label="Zulip"><svg width="20" height="20" viewBox="0 0 25 25" fill="none" xmlns="http://www.w3.org/2000/svg"><path d="M25 3.72273C25 4.98879 24.3687 6.10367 23.4007 6.78394L14.0783 14.2669C13.9099 14.3992 13.6785 14.1913 13.8047 14.0023L17.2348 7.86103C17.3401 7.69096 17.2138 7.4831 17.0034 7.4831H3.74579C1.6835 7.4831 0 5.80133 0 3.74163C0 1.68193 1.6835 0.000157697 3.74579 0.000157697H21.2542C23.3165 -0.0187386 25 1.66303 25 3.72273ZM3.74579 25H21.2542C23.3165 25 25 23.3182 25 21.2585C25 19.1988 23.3165 17.5171 21.2542 17.5171H7.99663C7.80724 17.5171 7.68098 17.3092 7.76515 17.1391L11.1953 10.9978C11.3215 10.8278 11.0901 10.601 10.9217 10.7333L1.59933 18.2162C0.631313 18.8776 0 19.9925 0 21.2585C0 23.3182 1.6835 25 3.74579 25Z" fill="white"></path></svg></a><a href="https://github.com/leanprover/" aria-label="GitHub"><img width="20" src="../../static/svg/github-white.svg" alt="GitHub"></a></div> 4118 </div> 4119 </footer>
4119<script src="-verso-data/theme.js"></script>
4119 4120
4120<script src="-verso-data/copy.js"></script>
4120 4121
4121<script src="-verso-data/motion.js"></script>
4121 4122
4122<script src="-verso-data/navbar.js"></script>
4122 4123
4123<script id="MathJax-script" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
4123 4124 </body> 4125 </html> 4126
Line numbers count LF bytes from the start of the resource, as the search results do. Vendor segments are library code the classifier recognised; they are stored but not indexed. Bytes are shown as Latin1 characters, one per byte.