Lean 4

https://github.com/leanprover/lean4
Admin
Lean 4 is a functional programming language and interactive theorem prover for writing verified...
Tokens:320,808
Snippets:2,477
Trust Score:9.7
License:Apache-2.0
Update:1 day ago
Show doc for...
Tokens:
Raw
### Install Lean source files

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Installs all .lean and .md files from the source directory to the build directory, excluding the examples directory. This is used for packaging the Lean source.

```cmake
install(
  DIRECTORY "${CMAKE_SOURCE_DIR}/"
  DESTINATION src/lean
  FILES_MATCHING
  PATTERN "*.lean"
  PATTERN "*.md"
  PATTERN examples EXCLUDE
)
```

--------------------------------

### Run and test the Web server from the command line

Source: https://github.com/leanprover/lean4/blob/master/tests/playground/webserver/README.md

The first command pipes a GET request into the Web server binary and shows the expected HTTP response. The second command starts the server with netcat to test in a browser at http://localhost:1234.

```bash
$ echo "GET /greet/me HTTP/1.1" | ./build/bin/Webserver
HTTP/1.1 200 OK
Content-Type: text/html
Content-Length: 19

<h1>Hello, me!</h1>

```

```bash
bash -c 'coproc nc -lp 1234; ./build/bin/Webserver <&${COPROC[0]} >&${COPROC[1]}'
```

--------------------------------

### Install build dependencies on Ubuntu

Source: https://github.com/leanprover/lean4/blob/master/doc/make/ubuntu.md

Run this command to install the required build tools and libraries for building Lean on Ubuntu. It uses apt-get to install git, libgmp-dev, libuv1-dev, libssl-dev, cmake, ccache, clang, and pkgconf.

```bash
sudo apt-get install git libgmp-dev libuv1-dev libssl-dev cmake ccache clang pkgconf
```

--------------------------------

### Lean docstring example for map with inline code examples

Source: https://github.com/leanprover/lean4/blob/master/doc/style.md

Shows a docstring for a constant `map` with a short summary, details, and a bulleted list of inline code examples. The examples are equalities that should be validated by various strategies.

```lean
/--
Applies the function `f` to each element of the list `xs`, returning a list of the results.

The results are in the same order as the corresponding inputs. This takes linear time: O(|`xs`|).

Examples:
* `map String.length ["a", "21", ""] = [1, 2, 0]`
* `map Nat.succ [] = []`
-/
@[specialize] def map (f : α → β) : (xs : List α) → List β
  | []  => []
  | a::as => f a :: map f as
```

--------------------------------

### Install license files for later stages

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Installs the LICENSE and LICENSES files to the installation root when building a later stage and INSTALL_LICENSE is enabled.

```cmake
if(STAGE GREATER 0 AND INSTALL_LICENSE)
  install(FILES "${CMAKE_SOURCE_DIR}/../LICENSE" "${CMAKE_SOURCE_DIR}/../LICENSES" DESTINATION ".")
endif()
```

--------------------------------

### Copy leanmake to bin and install bin directory

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Copies bin/leanmake into the build bin directory and installs the entire bin directory with source permissions.

```cmake
file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin)

install(DIRECTORY "${CMAKE_BINARY_DIR}/bin/" USE_SOURCE_PERMISSIONS DESTINATION bin)
```

--------------------------------

### Install elan on Windows

Source: https://github.com/leanprover/lean4/blob/master/doc/dev/index.md

Install elan on Windows without installing a default Lean toolchain. Run these commands in PowerShell.

```powershell
curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
powershell -f elan-init.ps1 --default-toolchain none
del elan-init.ps1
```

--------------------------------

### Install CADICAL and LEANTAR binaries

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Installs the CADICAL and LEANTAR programs to the bin directory when the respective conditions are met.

```cmake
if(STAGE GREATER 0 AND CADICAL AND INSTALL_CADICAL)
  install(PROGRAMS "${CADICAL}" DESTINATION bin)
endif()

if(LEANTAR AND INSTALL_LEANTAR)
  install(PROGRAMS "${LEANTAR}" DESTINATION bin)
endif()
```

--------------------------------

### Lean iterate function with input/output example blocks

Source: https://github.com/leanprover/lean4/blob/master/doc/style.md

Docstring for `iterate` with an example using alternating Lean input and output code blocks. The input is marked as Lean with `example` class and the output as `output`.

```lean
/--
Computes a value by iteration from a starting state `a`.

At each step, `f` is applied to the current state. `f` may return either a new state for further
iteration or a final value that stops iteration.

Example:
```lean
#eval iterate 6 fun x => do
  if x < 5 then
    pure (.inr ())
  else
    IO.println x
    pure (.inl (x - 1))
```
```output
6
5
```
-/
@[specialize] partial def iterate (a : α) (f : α → IO (Sum α β)) : IO β := do
  let v ← f a
  match v with
  | Sum.inl a => iterate a f
  | Sum.inr b => pure b
```

```lean
#eval iterate 6 fun x => do
  if x < 5 then
    pure (.inr ())
  else
    IO.println x
    pure (.inl (x - 1))
```

```output
6
5
```

--------------------------------

### Install elan on Unix

Source: https://github.com/leanprover/lean4/blob/master/doc/dev/index.md

Install elan on Unix without installing a default Lean toolchain. Use this command to set up elan for development.

```bash
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none
```

--------------------------------

### Docstring examples for axioms (propext and Classical.choice)

Source: https://github.com/leanprover/lean4/blob/master/doc/style.md

Two axiom docstrings showing the recommended format: begin with common names, provide an English statement, and optionally elaborate on consequences or special treatment. The Classical.choice example includes a warning about noncomputable definitions and the lack of algorithmic interpretation.

```lean
/--
Propositional Extensionality.

If two propositions are logically equivalent (that is, if each implies the other),
then they are equal; each may replace the other in all contexts.
-/
axiom propext {a b : Prop} : (a ↔ b) → a = b

/--
The Axiom of Choice.

`Nonempty α` is a proof that `α` has an element, but the element itself is
erased. The axiom `choice` supplies a particular element of `α` given only
this proof.

In particular, this axiom is
[global choice](https://en.wikipedia.org/wiki/Axiom_of_global_choice), which
is slightly stronger than the axiom of choice in ZFC.

The axiom of choice is used to derive the law of the excluded middle
(`Classical.em`), so it may show up in axiom listings for proofs that do
not obviously use choice.

This axiom can be used to construct “data” (that is, elements of non-Prop
types). There is no algorithmic interpretation of this axiom, so any definition
that would involve executing `Classical.choice` or other axioms must be marked
`noncomputable`. The compiler will not produce executable code for such
definitions, but they can be reasoned about in the logic.
-/
axiom Classical.choice {α : Sort u} : Nonempty α → α
```

--------------------------------

### HTML block with class attribute

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

A tag with attributes starts an HTML block.

```html
<i class="foo">
*bar*
</i>
```

--------------------------------

### Docstring examples for theorems (Eq.symm and Nat.ble_eq_true_of_le)

Source: https://github.com/leanprover/lean4/blob/master/doc/style.md

Two theorem docstrings demonstrating the recommended format: the /-- and -/ delimiters aligned with the declaration, English statement of the theorem, and proper indentation. The first example shows a one-line docstring for Eq.symm; the second shows a multi-line docstring for Nat.ble_eq_true_of_le.

```lean
/--
Equality is symmetric: if `a = b` then `b = a`.
-/
@[symm] theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a :=
  h ▸ rfl

/--
Propositional inequality of natural numbers implies Boolean inequality.
-/
theorem Nat.ble_eq_true_of_le (h : LE.le n m) : Eq (Nat.ble n m) true :=
  match h with
  | Nat.le.refl   => Nat.ble_self_eq_true n
  | Nat.le.step h => Nat.ble_succ_eq_true (ble_eq_true_of_le h)
```

--------------------------------

### HTML block with invalid tag start

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

The initial tag doesn't need to be valid, as long as it starts like one.

```html
<div *???-&&&-<---
*foo*
```

--------------------------------

### HTML block with closing tag

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

A closing tag can start an HTML block.

```html
</ins>
*bar*
```

--------------------------------

### HTML block with incomplete tag

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

The initial tag can be incomplete, as long as it starts like a tag.

```html
<div class
foo
```

--------------------------------

### Structure Subtype and Subarray examples with docstrings

Source: https://github.com/leanprover/lean4/blob/master/doc/style.md

Two structure examples with docstrings. The first documents `Subtype` with a type docstring and field docstrings for `val` and `property`. The second documents `Subarray` with a type docstring and field docstrings for `array`, `start`, `stop`, `start_le_stop`, and `stop_le_array_size`. Both follow the convention of describing fields by content.

```lean
/--
All the elements of some base type that satisfy a predicate.

`Subtype p`, usually written as `{x : α // p x}`, is a type which
represents all the elements `x : α` for which `p x` is true.
Logically, it is a pair-like type. If `v : α` and `h : p x`, then
`⟨v, h⟩ : {x // p x}`. There is a coercion from `⟨v, h⟩ : {x // p x}`
to `v : α`.
-/

@[pp_using_anonymous_constructor]
structure Subtype {α : Sort u} (p : α → Prop) where
  /--
  The underlying element in the base type.

  This is applied as a coercion when the expected type is `α`.
  -/
  val : α
  /--
  The value `val` satisfies the predicate.
  -/
  property : p val
```

```lean
/--
A section or “slice” of an array that shares the underlying memory allocation.

Subarrays can be used to avoid unnecessary copying and allocation of arrays. However,
subarrays retain a reference to their underlying array. The existence of multiple
subarrays from the same array will thus prevent array operations from being optimized
into mutation, even if the subarrays are disjoint.
-/
structure Subarray (α : Type u) where
  /--
  The underlying array.
  -/
  array : Array α
  /--
  The first index in the subarray, inclusive.
  -/
  start : Nat
  /--
  The last index in the subarray, exclusive.
  -/
  stop : Nat
  /--
  The start of the subarray is not greater than the end.
  -/
  start_le_stop : start ≤ stop
  /--
  The end of the subarray is within bounds for the underlying array.
  -/
  stop_le_array_size : stop ≤ array.size
```

--------------------------------

### Example commit message

Source: https://github.com/leanprover/lean4/blob/master/doc/dev/commit_convention.md

A complete example commit message for a fix that adds declarations for operator<< in the kernel. It includes a subject, a body starting with 'This PR ', and a footer referencing the issue. The body explains the motivation and contrasts with previous behavior.

```text
fix: add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel

This PR adds declarations `operator<<` for raw printing.
The actual implementation of these two operators is outside of the
kernel. They are implemented in the file 'library/printer.cpp'.

We declare them in the kernel to prevent the following problem.
Suppose there is a file 'foo.cpp' that does not include 'library/printer.h',
but contains
```cpp
expr a;
...
std::cout << a << "\n";
...
```

The compiler does not generate an error message. It silently uses the
operator bool() to coerce the expression into a Boolean. This produces
counter-intuitive behavior, and may confuse developers.
```

--------------------------------

### HTML block with table tag

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

A table tag starts an HTML block that includes everything until a blank line or end of document.

```html
<table><tr><td>
foo
</td></tr></table>
```

--------------------------------

### Install ccache via Homebrew

Source: https://github.com/leanprover/lean4/blob/master/doc/make/osx-10.9.md

Installs ccache, a recommended package for caching compiler output to speed up builds.

```bash
brew install ccache
```

--------------------------------

### Example theorem with HashMap getElem

Source: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md

Shows a theorem about HashMap indexing with proof obligation. The algorithm yields Std.HashMap.getElem?_eq_optionSome_getElem_of_mem, shortened to Std.HashMap.getElem?_eq_some_getElem.

```lean
example {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
    [Inhabited β] {m : Std.HashMap α β} {a : α} {h' : a ∈ m} : m[a]? = some (m[a]'h') :=
  sorry
```

--------------------------------

### Install Lean dependencies with pacman

Source: https://github.com/leanprover/lean4/blob/master/doc/make/msys2.md

Installs all dependencies needed to compile Lean on Windows using MSYS2's pacman package manager. Run this in the MSYS2 CLANG64 shell.

```bash
pacman -S make python mingw-w64-clang-x86_64-cmake mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-ccache mingw-w64-clang-x86_64-libuv mingw-w64-clang-x86_64-gmp mingw-w64-clang-x86_64-openssl git unzip diffutils binutils
```

--------------------------------

### Example theorems Nat.mul_zero and Nat.zero_mul

Source: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md

Two theorems showing how traversal order affects naming. One name may be a prefix of another.

```lean
theorem Nat.mul_zero (n : Nat) : n * 0 = 0 := sorry
```

```lean
theorem Nat.zero_mul (n : Nat) : 0 * n = 0 := sorry
```

--------------------------------

### Configure Plugins in lakefile.toml

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Example of specifying a plugin target within a TOML configuration file.

```toml
name = "example"

[[lean_lib]]
name = "Plugin"

[[lean_exe]]
name = "exe"
plugins = ["Plugin:shared"] # i.e., @example/Plugin:shared
```

--------------------------------

### Install clang via Homebrew

Source: https://github.com/leanprover/lean4/blob/master/doc/make/osx-10.9.md

Installs clang and lld (LLVM linker) via Homebrew. This is an alternative to Apple's clang++ for building Lean.

```bash
brew install llvm lld
```

--------------------------------

### Install required packages via Homebrew

Source: https://github.com/leanprover/lean4/blob/master/doc/make/osx-10.9.md

Installs the required packages for building Lean: CMake, GMP, libuv, OpenSSL, and pkgconf. These are necessary dependencies.

```bash
brew install cmake
brew install gmp
brew install libuv
brew install openssl
brew install pkgconf
```

--------------------------------

### Install lib directory with exclusions

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Installs the build lib directory to the destination lib, excluding temp, .export, .hash, .trace, .rsp, and .filelist files.

```cmake
install(
  DIRECTORY "${CMAKE_BINARY_DIR}/lib/"
  DESTINATION lib
  PATTERN temp EXCLUDE
  PATTERN "*.export" EXCLUDE
  PATTERN "*.hash" EXCLUDE
  PATTERN "*.trace" EXCLUDE
  PATTERN "*.rsp" EXCLUDE
  PATTERN "*.filelist" EXCLUDE
)
```

--------------------------------

### HTML block with multiline attribute

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

An HTML block starts with a block-level tag and includes everything until a blank line or end of document. The tag can span multiple lines.

```html
<div id="foo" class="bar
  baz">
</div>
```

--------------------------------

### Build Target via CLI

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Example command to build a specific target using the Lake CLI.

```bash
$ lake build @example/exe
```

--------------------------------

### Example theorem with reverse prefix

Source: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md

Shows a theorem about reverse preserving prefix. The algorithm suggests List.IsPrefix.reverse_prefix_reverse, shortened to List.IsPrefix.reverse.

```lean
example : l₁ <+: l₂ → reverse l₁ <:+ reverse l₂ := sorry
```

--------------------------------

### Check clang and cmake versions

Source: https://github.com/leanprover/lean4/blob/master/doc/make/msys2.md

Verifies that clang and cmake are installed and accessible after installing dependencies.

```bash
clang --version
cmake --version
```

--------------------------------

### Install gcc via Homebrew

Source: https://github.com/leanprover/lean4/blob/master/doc/make/osx-10.9.md

Installs the GNU Compiler Collection (gcc) via Homebrew. This is one of the compiler options for building Lean, recommended if you prefer gcc over Apple's clang++.

```bash
brew install gcc
```

--------------------------------

### Build lean.js with Emscripten

Source: https://github.com/leanprover/lean4/blob/master/doc/make/emscripten.md

Run these commands to configure and build the asm.js and WebAssembly binaries. Requires Emscripten installed. Produces lean_js_js.js, lean_js_wasm.js, and lean_js_wasm.wasm in the shell/ directory.

```bash
mkdir -p build/emscripten
cd build/emscripten
emconfigure cmake ../../src -DCMAKE_BUILD_TYPE=Emscripten
make lean_js_js lean_js_wasm
```

--------------------------------

### Example theorem with List prefix head

Source: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md

Shows a theorem about list prefix and head. The algorithm suggests List.IsPrefix.head_eq_head_of_ne_nil, shortened to List.IsPrefix.head.

```lean
example {x y : List α} (h : x <+: y) (hx : x ≠ []) :
  x.head hx = y.head (h.ne_nil hx) := sorry
```

--------------------------------

### Set custom install prefix

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Allows setting a custom install prefix via the LEAN_INSTALL_PREFIX cache variable. If set, it appends the version name and system name to the prefix. The system name is lowercased.

```cmake
set(LEAN_INSTALL_PREFIX "" CACHE STRING "If set, set CMAKE_INSTALL_PREFIX to this value + version name")
if(LEAN_INSTALL_PREFIX)
  string(TOLOWER ${CMAKE_SYSTEM_NAME} LOWER_SYSTEM_NAME)
  set(
    LEAN_INSTALL_SUFFIX
    "-${LOWER_SYSTEM_NAME}"
    CACHE STRING
    "If LEAN_INSTALL_PREFIX is set, append this value to CMAKE_INSTALL_PREFIX"
  )
  set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}")
endif()
```

--------------------------------

### HTML output for blockquote with list and continuation

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

The HTML output for the preceding blockquote example, showing a blockquote containing a list item with two paragraphs.

```html
<blockquote>
<ul>
<li>
<p>one</p>
<p>two</p>
</li>
</ul>
</blockquote>
```

--------------------------------

### HTML output for list with less-indented continuation

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

The HTML output for the preceding Markdown example, showing a single list item with two paragraphs.

```html
<ul>
<li>
<p>one</p>
<p>two</p>
</li>
</ul>
```

--------------------------------

### Syntax category json example with docstring

Source: https://github.com/leanprover/lean4/blob/master/doc/style.md

Example of documenting a syntax category with a noun phrase docstring. The docstring is a single sentence without punctuation, as recommended for noun phrases.

```lean
/-- JSON literals -/
declare_syntax_cat json (behavior := symbol)
```

--------------------------------

### Adding a Mathlib Dependency

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Example of adding a mathlib dependency to a Lake package configuration.

```lean
package hello

require "leanprover-community" / "mathlib"
```

--------------------------------

### Inductive List example with docstrings

Source: https://github.com/leanprover/lean4/blob/master/doc/style.md

Example of documenting an inductive type with a docstring for the type and constructors. The type docstring uses a noun phrase and references the manual. Constructor docstrings describe the empty list and cons cell, including notation.

```lean
/--
A linked list with elements of type `α`.

Like `Array`, `List` represents an ordered sequence. Their performance
characteristics differ, however, and are described in [the Lean Language Reference](manual://...).
-/
inductive List (α : Type u) where
  /-- The empty list, typically written `[]`. -/
  | nil : List α
  /--
  A list in which the first element is `head` and the rest of the list is `tail`,
  typically written `head :: tail`.
  -/
  | cons (head : α) (tail : List α) : List α
```

--------------------------------

### Syntax and structure declarations for JSON and rintro patterns

Source: https://github.com/leanprover/lean4/blob/master/doc/style.md

Shows Lean syntax declarations for JSON and rintro patterns, a structure definition for a bijection, and an infix notation with a recommended spelling. The example demonstrates how to document syntax rules and structures with docstrings.

```lean
/-- JSON array -/
syntax "[" json,* "]" : json
/--
JSON identifier.

This is used as a key in an object.
-/
syntax jsonIdent := ident <|> str
/-- JSON key/value pair -/
syntax jsonField := jsonIdent ": " json
/-- JSON object -/
syntax "{" jsonField,* "}" : json

/-- A JSON literal as a Lean term -/
syntax "json% " json : term

/-- An `rcases` pattern is an `rintro` pattern -/
syntax (name := rintroPat.one) rcasesPat : rintroPat
/--
A multi-argument binder for a sequence of patterns.

The pattern `(pat1 ... : ty)` binds the variables in the pattern and ensures that each
has type `ty`.
-/
syntax (name := rintroPat.binder) (priority := default+1) -- to override rcasesPat.paren
  "(" rintroPat+ (" : " term)? ")" : rintroPat

/--
A bijection between two types is a pair of mutually inverse functions between them.
-/
structure Bijection (α β) where
  into : α → β
  outOf : β → α
  /- Properties omitted -/

@[inherit_doc Bijection]
infix:50 " ⇔ " => Bijection

recommended_spelling "bij" for "⇔" in [Bijection, «term_⇔_»]
```

--------------------------------

### Markdown equivalent list example with indented block and nested list

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

Equivalent Markdown version of the AsciiDoc example, showing list item continuation with an indented block containing shell commands and a nested ordered list. Demonstrates Markdown's readability through visible nesting.

```markdown
1.  List item one.

    List item one continued with a second paragraph followed by an
    Indented block.

        $ ls *.sh
        $ mv *.sh ~/tmp

    List item continued with a third paragraph.

2.  List item two continued with an open block.

    This paragraph is part of the preceding list item.

    1. This list is nested and does not require explicit item continuation.

       This paragraph is part of the preceding list item.

    2. List item b.

    This paragraph belongs to item two of the outer list.
```

--------------------------------

### Example of interactive test with completion request

Source: https://github.com/leanprover/lean4/blob/master/tests/README.md

Shows how to mark a position in a .lean file for an LSP request. The --^ marker points to the line where the request is simulated, here a completion request at 'Bla.'.

```lean
open Foo in
theorem tst2 (h : a ≤ b) : a + 2 ≤ b + 2 :=
Bla.
  --^ completion
```

--------------------------------

### Build and run the package

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Commands to build the package and execute the resulting binary.

```bash
$ lake build
...
$ ./.lake/build/bin/hello
Hello, world!
```

--------------------------------

### Class HAdd example with docstrings

Source: https://github.com/leanprover/lean4/blob/master/doc/style.md

Example of documenting a class declaration with a docstring for the class and the `hAdd` method. The class docstring explains the notation `+` and the meaning of heterogeneous addition. The method docstring describes the operation and its dependence on types.

```lean
/--
Addition of two terms that don't necessarily have the same type. Instances are used to assign
meaning to the `+` operator.

`HAdd` is short for "heterogeneous addition."
-/
class HAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /--
  `a + b` computes the sum of `a` and `b`.

  The precise meaning of this operation depends on the types of `a`, `b`, and the
  entire term.
  -/
  hAdd : α → β → γ
```

--------------------------------

### Info string with extra attributes

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

The info string may contain additional words after the language name. The first word is used for the language class; the rest are ignored in this example.

```markdown
~~~~    ruby startline=3 $%@#$
def foo(x)
  return 3
end
~~~~~~~

```

```html
<pre><code class="language-ruby">def foo(x)
  return 3
end
</code></pre>

```

--------------------------------

### Initialize a new package with lake init

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Create a new package in the current directory using the lake init command.

```bash
$ mkdir hello
$ cd hello
$ lake init hello
```

--------------------------------

### Configuration files for elab test pile

Source: https://github.com/leanprover/lean4/blob/master/tests/README.md

These files configure a test: `<file>.init.sh` is sourced at start, `<file>.before.sh` is executed before the test, `<file>.after.sh` is executed after, `<file>.out.expected` contains expected output, and `<file>.out.ignored` ignores output comparison.

```bash
<file>.init.sh
```

```bash
<file>.before.sh
```

```bash
<file>.after.sh
```

```bash
<file>.out.expected
```

```bash
<file>.out.ignored
```

--------------------------------

### Specify Targets in lakefile.lean

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Example of using literal target specifiers in a Lean configuration file.

```lean
package "example"

input_file foo where
  path := "inputs/foo.txt"
  text := true

@[default_target]
lean_exe exe where
  needs := #[`@/foo] -- i.e., `@examole/foo
```

--------------------------------

### Command to build header snapshots

Source: https://github.com/leanprover/lean4/blob/master/tests/README.md

Run this command to build prebuilt header snapshots before manually running tests with `LEAN_HEADER_SNAPSHOTS=1`.

```bash
tests/with_stage1_test_env.sh tests/build_lean_header_snapshots.sh
```

--------------------------------

### HTML output for two lists with intervening paragraph

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

The HTML output produced by the four-space rule for the preceding Markdown example, showing two separate lists with a paragraph between them.

```html
<ul>
<li>foo</li>
</ul>
<p>bar</p>
<ul>
<li>baz</li>
</ul>
```

--------------------------------

### Build directory structure

Source: https://github.com/leanprover/lean4/blob/master/doc/dev/bootstrap.md

Shows the layout of the build directory with stage0, stage1, and stage2/3 subdirectories, including the key files and their roles in the bootstrapping process.

```bash
stage0/
  # Bootstrap binary built from stage0/src/.
  # We do not use any other files from this directory in further stages.
  bin/lean
stage1/
  include/
    config.h  # config variables used to build `lean` such as used allocator
    runtime/lean.h  # runtime header, used by extracted C code, uses `config.h`
  share/lean/
    lean.mk  # used by `leanmake`
  lib/
    lean/**/*.olean  # the Lean library (incl. the compiler) compiled by the previous stage's `lean`
    temp/**/*.{c,o}  # the library extracted to C and compiled by `leanc`
    libInit.a libLean.a  # static libraries of the Lean library
    libleancpp.a  # a static library of the C++ sources of Lean
    libleanshared.so  # a dynamic library including the static libraries above
  bin/
    lean  # the Lean compiler & server, a small executable that calls directly into libleanshared.so
    leanc  # a wrapper around a C compiler supplying search paths etc
    leanmake  # a wrapper around `make` supplying the Makefile above
stage2/...
stage3/...
```

--------------------------------

### HTML block with partial tag

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

A partial tag need not be completed; the block includes everything until a blank line or end of document.

```html
<div id="foo"
*hi*
```

--------------------------------

### HTML block with del tag on its own line

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

When the <del> tag is on a line by itself, it starts a raw HTML block.

```html
<del>
*foo*
</del>
```

--------------------------------

### Initialize a new package with lake new

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Create a new package in a new directory using the lake new command.

```bash
$ lake new hello
$ cd hello
```

--------------------------------

### Lean docstring for dite with dependent if-then-else explanation

Source: https://github.com/leanprover/lean4/blob/master/doc/style.md

Docstring for `dite` explaining the dependent if-then-else and its use in bounds checking. Includes an example of lifting a bounds check to a branch.

```lean
/--
Checks whether the provided proposition `c` is true or false and invokes the corresponding
branch `t` or `e` with a suitable proof.

The "dependent" `if-then-else`, normally written via the notation `if h : c then t else e`, is
syntactic sugar for `dite c (fun h => t) (fun h => e)`. As a result, the code in each branch
can observe the truth or falsity of the condition.

For example, `GetElem.getElem arr i h`, normally written `arr[i]` with `h` found automatically,
expects a proof `h : i < arr.size` in order to avoid a bounds check. This bounds check can be
lifted to a branch: `if h : i < arr.size then arr[h] else ...`, and one bounds check can be used
for multiple array accesses.
-/
@[macro_inline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α :=
  h.casesOn e t
```

--------------------------------

### Run spec tests with spec_tests.py

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

Command to run the Markdown conformance tests against a program using the spec_tests.py script. Replace PROGRAM with the path to the Markdown implementation being tested.

```bash
python test/spec_tests.py --spec spec.txt --program PROGRAM
```

--------------------------------

### Create leanrt_initial-exec static library

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/runtime/CMakeLists.txt

Creates a static library 'leanrt_initial-exec' from the runtime objects, built with the default -ftls-model=initial-exec, and places the archive in the current binary directory.

```cmake
add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
set_target_properties(leanrt_initial-exec PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})
```

--------------------------------

### HTML block with tag on next line

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

The initial tag can be split across lines; the block continues until a blank line or end of document.

```html
<div
> not quoted text
```

--------------------------------

### HTML block with non-block-level tag on its own line

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

To start an HTML block with a tag not in the block-level list, the tag must be on its own line and complete.

```html
<a href="foo">
*bar*
</a>
```

--------------------------------

### List wrapping in <p> tags ambiguity

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

Illustrates the ambiguity of when list items get wrapped in <p> tags, showing a partially loose list.

```markdown
1. one

2. two
3. three
```

--------------------------------

### HTML block containing Markdown code fence

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

Everything until the next blank line or end of document gets included in the HTML block, so a Markdown code fence is part of the HTML block.

```html
<div></div>
``` c
int x = 33;
```
```

--------------------------------

### Run the generated test program

Source: https://github.com/leanprover/lean4/blob/master/doc/examples/compiler/README.md

Execute the compiled test program with arguments 'hello' and 'world'. The expected output is 'Result: [hello, world]'.

```bash
./build/bin/test hello world
```

--------------------------------

### Run Cross benchmark suite with Nix

Source: https://github.com/leanprover/lean4/blob/master/tests/bench/README.md

Builds and runs the Cross benchmark suite using Nix and make, recording 50 runs per configuration and generating CSV and HTML reports.

```bash
nix develop
make
```

--------------------------------

### Define leancpp_1 and leancpp static libraries

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Creates two static libraries from LEAN_OBJS. leancpp_1 omits the initialize object, while leancpp includes it via $<TARGET_OBJECTS:initialize>. Both set ARCHIVE_OUTPUT_DIRECTORY to lib/temp and OUTPUT_NAME accordingly.

```cmake
  # leancpp without `initialize` (see `leaninitialize` above)
  add_library(leancpp_1 STATIC ${LEAN_OBJS})
  set_target_properties(
    leancpp_1
    PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp OUTPUT_NAME leancpp_1
  )
  add_library(leancpp STATIC ${LEAN_OBJS} $<TARGET_OBJECTS:initialize>)
  set_target_properties(leancpp PROPERTIES OUTPUT_NAME leancpp)
endif()
```

--------------------------------

### Clean stdlib and cache-get targets

Source: https://github.com/leanprover/lean4/blob/master/CMakeLists.txt

Defines clean-stdlib and cache-get targets that depend on stage1-configure. The install target runs make -C stage1 install during installation.

```cmake
add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1-configure)
```

```cmake
add_custom_target(cache-get COMMAND $(MAKE) -C stage1 cache-get DEPENDS stage1-configure)
```

```cmake
install(CODE "execute_process(COMMAND make -C stage1 install)")
```

--------------------------------

### Namespace placement examples: List.Sublist.reverse and List.reverse_sublist

Source: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md

Place theorems in the most specific namespace appearing in a hypothesis. The first theorem has a hypothesis of type List.Sublist, so it goes in List.Sublist; the second does not, so it goes in List. This enables generalized projection notation like h.reverse.

```lean
theorem List.Sublist.reverse : l₁ <+ l₂ → l₁.reverse <+ l₂.reverse := sorry
```

```lean
theorem List.reverse_sublist : l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂ := sorry
```

--------------------------------

### Visualize profile data with hotspot

Source: https://github.com/leanprover/lean4/blob/master/doc/perf.md

Launches the hotspot GUI to visualize the profiling data collected by perf. Run after the perf record command.

```bash
hotspot
```

--------------------------------

### Hello/Basic.lean module file

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

A basic library module file containing a simple definition.

```lean
def hello := "world"
```

--------------------------------

### Footer issue reference example

Source: https://github.com/leanprover/lean4/blob/master/doc/dev/commit_convention.md

Example of how to reference closed issues in the footer, using the 'Closes' keyword followed by issue numbers.

```text
Closes #123, #456
```

--------------------------------

### Basic parallelized release build

Source: https://github.com/leanprover/lean4/blob/master/doc/make/index.md

Clones the Lean 4 repository and performs a basic parallelized release build. Replace `$(nproc || sysctl -n hw.logicalcpu)` with the desired parallelism amount. The build outputs to the `stage1` subfolder.

```bash
git clone https://github.com/leanprover/lean4
cd lean4
cmake --preset release
make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)
```

--------------------------------

### Main.lean executable entry point

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

The main file of the executable containing the main function.

```lean
import «Hello»

def main : IO Unit :=
  IO.println s!"Hello, {hello}!"
```

--------------------------------

### Both left and right-flanking delimiter runs

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

Examples of delimiter runs that are both left-flanking and right-flanking, as defined by the spec.

```markdown
 abc***def
"abc"_"def"
```

--------------------------------

### Right-flanking but not left-flanking delimiter runs

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

Examples of delimiter runs that are right-flanking but not left-flanking, as defined by the spec.

```markdown
 abc***
 abc_
"abc"**
"abc"_
```

--------------------------------

### Run full benchmark suite

Source: https://github.com/leanprover/lean4/blob/master/tests/README.md

Runs the full benchmark suite and produces tests/measurements.jsonl.

```sh
make -C build/release -j "$(nproc)" bench # produces tests/measurements.jsonl
```

--------------------------------

### Left-flanking but not right-flanking delimiter runs

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

Examples of delimiter runs that are left-flanking but not right-flanking, as defined by the spec.

```markdown
***abc
  _abc
**"abc"
 _"abc"
```

--------------------------------

### Build Lake with build.sh

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Use the build.sh script to compile Lake, optionally passing parallel build flags like -j4.

```bash
$ ./build.sh -j4
```

--------------------------------

### Neither left nor right-flanking delimiter runs

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

Examples of delimiter runs that are neither left-flanking nor right-flanking, as defined by the spec.

```markdown
abc *** def
a _ b
```

--------------------------------

### Define leaninitialize and leanshell static libraries

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Creates static libraries leaninitialize and leanshell, setting their output directories and names. On Windows, appends linker flags for whole-archive linking of leanmanifest.

```cmake
add_library(leaninitialize STATIC $<TARGET_OBJECTS:initialize>)
set_target_properties(
  leaninitialize
  PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp OUTPUT_NAME leaninitialize
)
add_library(leanshell STATIC util/shell.cpp)
set_target_properties(leanshell PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp OUTPUT_NAME leanshell)
if(CMAKE_SYSTEM_NAME MATCHES "Windows")
  string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,--whole-archive -lleanmanifest -Wl,--no-whole-archive")
endif()
```

--------------------------------

### Run the release checklist script

Source: https://github.com/leanprover/lean4/blob/master/doc/dev/release.md

Run the interactive release checklist script from the script/release directory. Use -i/--interactive to enable modifications; without it, it only reports status. Requires membership in lean-release-managers teams and write access to specific repos.

```bash
cd script/release
uv run checklist.py v4.X.Y -i
```

--------------------------------

### Correct Lean file structure with copyright, prelude, imports, module doc, and universes

Source: https://github.com/leanprover/lean4/blob/master/doc/std/style.md

Use this structure for every Lean file. It shows the required order: copyright header, prelude declaration, imports, module documentation string, and optional universe variable declarations. There should be no blank line between the copyright header and imports, but a blank line between imports and the module documentation string.

```lean
/-
Copyright (c) 2014 Parikshit Khanna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro,
  Yury Kudryashov
-/
prelude
import Init.Data.List.Pairwise
import Init.Data.List.Find

/-!
**# Lemmas about `List.eraseP` and `List.erase`.**
-/

universe u u'
```

--------------------------------

### Configure leanc.sh and Leanc.lean

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Configures leanc.sh from bin/leanc.in and, for stage > 0 and non-Emscripten, configures Leanc.lean and builds the leanc target. The leanc target depends on leanshared and runs make -f stdlib.make leanc.

```cmake
configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/leanc.sh" @ONLY)
if(STAGE GREATER 0 AND NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
  configure_file("${LEAN_SOURCE_DIR}/Leanc.lean" "${CMAKE_BINARY_DIR}/leanc/Leanc.lean" @ONLY)
  add_custom_target(
    leanc
    ALL
    WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/leanc
    DEPENDS leanshared
    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanc
    VERBATIM
  )
  if(TARGET lean-beam)
    add_dependencies(lean-beam lake leanc)
  endif()
endif()
```

--------------------------------

### Define leanmain and leanmanifest static libraries

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/shell/CMakeLists.txt

Defines the static libraries `leanmain` and `leanmanifest`. `leanmanifest` includes a generated empty C file (created with `file(CONFIGURE ...)` to avoid touching the file on each run) and `manifest.rc`; both libraries are placed in specific output directories.

```cmake
add_library(leanmain STATIC lean.cpp)
set_target_properties(leanmain PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp OUTPUT_NAME leanmain)

# library must contain at least one non-manifest file
# We use `CONFIGURE` instead of `WRITE` so as to avoid touching the file on each run
file(CONFIGURE OUTPUT ${CMAKE_BINARY_DIR}/temp/empty.c CONTENT "")
add_library(leanmanifest STATIC ${CMAKE_BINARY_DIR}/temp/empty.c manifest.rc)
set_target_properties(
  leanmanifest
  PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/lean OUTPUT_NAME leanmanifest
)
```

--------------------------------

### Fenced code block between heading and setext heading

Source: https://github.com/leanprover/lean4/blob/master/tests/markdown_conformance/spec.txt

Other blocks can occur before and after a fenced code block without an intervening blank line. The example shows a setext heading, code block, and ATX heading.

```markdown
foo
---
~~~
bar
~~~
# baz

```

```html
<h2>foo</h2>
<pre><code>bar
</code></pre>
<h1>baz</h1>

```

--------------------------------

### Import and copy C++ libraries for later stages

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

For stages greater than 1, imports static libraries leanrt_initial-exec, leanrt, leancpp_1, and leancpp, and defines a custom target to copy them from the previous stage. Adds dependencies and optionally copies lean.h.bc when LLVM is enabled.

```cmake
if(STAGE GREATER 1)
  # reuse C++ parts, which don't change
  add_library(leanrt_initial-exec STATIC IMPORTED)
  set_target_properties(
    leanrt_initial-exec
    PROPERTIES IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a"
  )
  add_library(leanrt STATIC IMPORTED)
  set_target_properties(leanrt PROPERTIES IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a")
  add_library(leancpp_1 STATIC IMPORTED)
  set_target_properties(leancpp_1 PROPERTIES IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/temp/libleancpp_1.a")
  add_library(leancpp STATIC IMPORTED)
  set_target_properties(leancpp PROPERTIES IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
  add_custom_target(
    copy-leancpp
    COMMAND
      ${CMAKE_COMMAND} -E copy_if_different "${PREV_STAGE}/runtime/libleanrt_initial-exec.a"
      "${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a"
    COMMAND ${CMAKE_COMMAND} -E copy_if_different "${PREV_STAGE}/lib/lean/libleanrt.a" "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a"
    COMMAND ${CMAKE_COMMAND} -E copy_if_different "${PREV_STAGE}/lib/lean/libleancpp.a" "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a"
    COMMAND
      ${CMAKE_COMMAND} -E copy_if_different "${PREV_STAGE}/lib/temp/libleancpp_1.a" "${CMAKE_BINARY_DIR}/lib/temp/libleancpp_1.a"
  )
  add_dependencies(leanrt_initial-exec copy-leancpp)
  add_dependencies(leanrt copy-leancpp)
  add_dependencies(leancpp_1 copy-leancpp)
  add_dependencies(leancpp copy-leancpp)
  if(LLVM)
    add_custom_target(
      copy-lean-h-bc
      COMMAND ${CMAKE_COMMAND} -E copy_if_different "${PREV_STAGE}/lib/lean/lean.h.bc" "${CMAKE_BINARY_DIR}/lib/lean/lean.h.bc"
    )
    add_dependencies(leancpp copy-lean-h-bc)
  endif()
else()
  if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
    add_dependencies(leanrt libuv)
    add_dependencies(leanrt_initial-exec libuv)
  endif()

  add_subdirectory(util)
  set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:util>)
  add_subdirectory(kernel)
  set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:kernel>)
  add_subdirectory(library)
  set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:library>)
  add_subdirectory(library/constructions)
  set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:constructions>)
endif()
```

--------------------------------

### Open repository in VS Code

Source: https://github.com/leanprover/lean4/blob/master/doc/dev/index.md

Open the repository folder in VS Code from the command line. The `.vscode/` directory provides settings, tasks, and recommended extensions.

```bash
code .
```

--------------------------------

### Reference Targets by Identifier in lakefile.lean

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Example of specifying targets by their identifier within a Lean configuration file.

```lean
input_file foo where
  path := "inputs/foo.txt"
  text := true

lean_exe exe where
  needs := #[foo]
```
Tokens:
Raw