========================
CODE SNIPPETS
========================
TITLE: Installing Files with CMake
DESCRIPTION: This CMake code installs files from the source directory to the destination directory. It uses the `install(DIRECTORY)` command to install files matching specific patterns, such as `.lean` and `.md` files, while excluding the `examples` directory. The `FILES_MATCHING` argument specifies the patterns to include or exclude.

SOURCE: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt#_snippet_96

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

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

TITLE: Basic File Structure Example
DESCRIPTION: This example demonstrates the basic structure of a Lean 4 file, including the copyright header, imports, module documentation, and universe variable declarations.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/style.md#_snippet_8

LANGUAGE: lean
CODE:
```
/-
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'
```

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

TITLE: Install elan without default Lean (Windows)
DESCRIPTION: This set of commands installs elan without installing a default version of Lean on Windows. It uses curl to download the elan-init.ps1 script, executes it with PowerShell, and then deletes the script.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/dev/index.md#_snippet_1

LANGUAGE: powershell
CODE:
```
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
```

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

TITLE: Executing Lean Examples
DESCRIPTION: This command executes a simple set of examples using the Lean executable located in the bin directory. It assumes the user is in the same directory as the Lean binary distribution.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/bin/README.md#_snippet_0

LANGUAGE: Shell
CODE:
```
% bin/lean examples/ex.lean
```

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

TITLE: Install elan without default Lean (Unix)
DESCRIPTION: This command installs elan without installing a default version of Lean on Unix-like systems. It uses curl to download the elan-init.sh script and executes it with the --default-toolchain none option.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/dev/index.md#_snippet_0

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

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

TITLE: LaTeX Example with Minted Package
DESCRIPTION: This LaTeX example demonstrates how to use the 'minted' package for Lean 4 code highlighting. It requires installing Pygments and using XeLaTeX or LuaLaTeX for Unicode support. The example defines a custom minted environment for Lean 4 code.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/syntax_highlight_in_latex.md#_snippet_2

LANGUAGE: LaTeX
CODE:
```
\documentclass{article}
\usepackage{fontspec}
% switch to a monospace font supporting more Unicode characters
\setmonofont{FreeMono}
\usepackage{minted}
\newmintinline[lean]{lean4}{bgcolor=white}
\newminted[leancode]{lean4}{fontsize=\footnotesize}
\usemintedstyle{tango}  % a nice, colorful theme

\begin{document}
\begin{leancode}
theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := by
  show extfunApp (Quotient.mk' f₁) = extfunApp (Quotient.mk' f₂)
  apply congrArg
  apply Quotient.sound
  exact h
\end{leancode}
\end{document}
```

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

TITLE: Documenting Axiom with Description in Lean 4
DESCRIPTION: This example demonstrates how to document an axiom in Lean 4, including a description of the axiom's purpose and implications.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/style.md#_snippet_2

LANGUAGE: Lean
CODE:
```
/--
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
```

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

TITLE: Documenting Theorem with Pattern Matching in Lean 4
DESCRIPTION: This example demonstrates how to document a theorem in Lean 4, including a description of the theorem's statement in English and the use of pattern matching.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/style.md#_snippet_1

LANGUAGE: Lean
CODE:
```
/--
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)
```

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

TITLE: Install Lean Dependencies using Pacman
DESCRIPTION: This command uses the pacman package manager in MSYS2 to install the necessary dependencies for compiling Lean, including make, python, cmake, clang, ccache, libuv, gmp, git, unzip, diffutils, and binutils.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/make/msys2.md#_snippet_0

LANGUAGE: bash
CODE:
```
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 git unzip diffutils binutils
```

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

TITLE: Adding Lean Compiler Documentation Example Test
DESCRIPTION: Adds a test for the Lean compiler's documentation example, running `leanmake --always-make` in the `doc/examples/compiler` directory and then executing the resulting binary.

SOURCE: https://github.com/leanprover/lean4/blob/master/stage0/src/shell/CMakeLists.txt#_snippet_17

LANGUAGE: CMake
CODE:
```
add_test(NAME leancomptest_doc_example
         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples/compiler"
         COMMAND bash -c "export ${TEST_VARS}; leanmake --always-make bin && ./build/bin/test hello world")
```

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

TITLE: Installing Basic Packages on Ubuntu
DESCRIPTION: This command installs essential packages required for building Lean on Ubuntu. It includes git, libgmp-dev, libuv1-dev, cmake, ccache, clang, and pkgconf.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/make/ubuntu.md#_snippet_0

LANGUAGE: bash
CODE:
```
sudo apt-get install git libgmp-dev libuv1-dev cmake ccache clang pkgconf
```

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

TITLE: Documenting Theorem with Attributes in Lean 4
DESCRIPTION: This example demonstrates how to document a theorem in Lean 4, including a description of the theorem's statement in English and the use of the `@[symm]` attribute.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/style.md#_snippet_0

LANGUAGE: Lean
CODE:
```
/--
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
```

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

TITLE: Install Command
DESCRIPTION: This snippet defines an installation command that executes a make command in the `stage1` directory to install the project.

SOURCE: https://github.com/leanprover/lean4/blob/master/CMakeLists.txt#_snippet_15

LANGUAGE: CMake
CODE:
```
install(CODE "execute_process(COMMAND make -C stage1 install)")
```

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

TITLE: Installing Directories and Files
DESCRIPTION: This snippet installs the include and share directories, and configures and installs the `lean.mk` file.

SOURCE: https://github.com/leanprover/lean4/blob/master/stage0/src/CMakeLists.txt#_snippet_62

LANGUAGE: CMake
CODE:
```
install(DIRECTORY ${LEAN_BINARY_DIR}/include/ DESTINATION include)
configure_file(${LEAN_SOURCE_DIR}/lean.mk.in ${LEAN_BINARY_DIR}/share/lean/lean.mk)
install(DIRECTORY ${LEAN_BINARY_DIR}/share/ DESTINATION share)
```

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

TITLE: Example Lean module definition
DESCRIPTION: This Lean code defines a simple string named `hello` with the value "world". This is a basic example of a module definition in Lean.

SOURCE: https://github.com/leanprover/lean4/blob/master/src/lake/README.md#_snippet_3

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

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

TITLE: Installing Libraries
DESCRIPTION: Installs the libraries from the binary directory to the installation directory, excluding temporary files, export files, hash files, trace files, and response files.

SOURCE: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt#_snippet_94

LANGUAGE: CMake
CODE:
```
install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib
  PATTERN temp EXCLUDE
  PATTERN "*.export" EXCLUDE
  PATTERN "*.hash" EXCLUDE
  PATTERN "*.trace" EXCLUDE
  PATTERN "*.rsp" EXCLUDE)
```

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

TITLE: Open VS Code workspace
DESCRIPTION: This command opens the `lean.code-workspace` file in VS Code, which configures the editor with workspace roots for the stage0/stage1 setup and other settings.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/dev/index.md#_snippet_3

LANGUAGE: bash
CODE:
```
code lean.code-workspace
```

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

TITLE: Copying and Installing Leanmake Executable
DESCRIPTION: This snippet copies the `leanmake` executable from the source directory to the binary directory and installs the contents of the binary directory into the `bin` destination.

SOURCE: https://github.com/leanprover/lean4/blob/master/stage0/src/CMakeLists.txt#_snippet_82

LANGUAGE: CMake
CODE:
```
file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin)

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

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

TITLE: Installing Directories
DESCRIPTION: This snippet installs the include and share directories.

SOURCE: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt#_snippet_64

LANGUAGE: CMake
CODE:
```
install(DIRECTORY ${LEAN_BINARY_DIR}/include/ DESTINATION include)
configure_file(${LEAN_SOURCE_DIR}/lean.mk.in ${LEAN_BINARY_DIR}/share/lean/lean.mk)
install(DIRECTORY ${LEAN_BINARY_DIR}/share/ DESTINATION share)
```

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

TITLE: HashMap Example Theorem Naming in Lean4
DESCRIPTION: This example demonstrates the naming algorithm for a theorem related to `Std.HashMap` in Lean4. It showcases the initial name generated by the algorithm and the subsequent shortening process based on context and clarity.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md#_snippet_4

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

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

TITLE: Theorem Declaration Example
DESCRIPTION: This example shows the correct indentation and formatting for a multi-line theorem declaration in Lean 4. The colon indicating the type should not be at the start of a line.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/style.md#_snippet_9

LANGUAGE: lean
CODE:
```
theorem eraseP_eq_iff {p} {l : List α} :
    l.eraseP p = l' ↔
      ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨
        ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧
          l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ :=
  sorry
```

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

TITLE: Verify CMake Version
DESCRIPTION: This command checks the installed version of CMake. It verifies that CMake is correctly installed and accessible in the MSYS2 environment.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/make/msys2.md#_snippet_2

LANGUAGE: bash
CODE:
```
cmake --version
```

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

TITLE: Running the Web Server
DESCRIPTION: This bash command executes the compiled Lean 4 web server and sends a sample HTTP request to it. It demonstrates how to interact with the server via standard input and output.

SOURCE: https://github.com/leanprover/lean4/blob/master/tests/playground/webserver/README.md#_snippet_0

LANGUAGE: bash
CODE:
```
echo "GET /greet/me HTTP/1.1" | ./build/bin/Webserver
```

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

TITLE: Checking Lambda Abstraction Examples in Lean
DESCRIPTION: These examples demonstrate how to define lambda abstractions in Lean using both the `fun` and `λ` keywords. They show the basic syntax for creating functions that take a natural number as input and return the result of adding 5 to it.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/funabst.md#_snippet_0

LANGUAGE: lean
CODE:
```
#check fun (x : Nat) => x + 5
#check λ (x : Nat) => x + 5
#check fun x : Nat => x + 5
#check λ x : Nat => x + 5
```

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

TITLE: Verify Clang Version
DESCRIPTION: This command checks the installed version of the clang compiler. It verifies that clang is correctly installed and accessible in the MSYS2 environment.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/make/msys2.md#_snippet_1

LANGUAGE: bash
CODE:
```
clang --version
```

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

TITLE: Building and running the Lake package
DESCRIPTION: This command builds the Lake package and then executes the resulting binary, which prints "Hello, world!" to the console.

SOURCE: https://github.com/leanprover/lean4/blob/master/src/lake/README.md#_snippet_7

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

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

TITLE: Displaying lake help
DESCRIPTION: This command displays the help information for the lake package manager, listing available commands and options.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/setup.md#_snippet_3

LANGUAGE: sh
CODE:
```
lake help
```

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

TITLE: Initializing a Lean Package with lake
DESCRIPTION: This command initializes a new Lean package named 'foo' in the current directory using the lake package manager. It sets up the basic directory structure and configuration files.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/setup.md#_snippet_1

LANGUAGE: sh
CODE:
```
lake init foo
```

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

TITLE: Building and Running Cross Suite with Nix
DESCRIPTION: Builds and runs the Cross benchmark suite using Nix. This command sets up the environment and executes the benchmarks.

SOURCE: https://github.com/leanprover/lean4/blob/master/tests/bench/README.md#_snippet_2

LANGUAGE: Shell
CODE:
```
nix develop
make
```

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

TITLE: Where Clause Example
DESCRIPTION: This example demonstrates the correct indentation and formatting for `where` clauses in Lean 4. The `where` keyword is unindented, and the declarations bound by it are indented by two spaces.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/style.md#_snippet_14

LANGUAGE: lean
CODE:
```
@[simp] theorem partition_eq_filter_filter (p : α → Bool) (l : List α) :
    partition p l = (filter p l, filter (not ∘ p) l) := by
  simp [partition, aux]
where
  aux (l) {as bs} : partition.loop p l (as, bs) =
      (as.reverse ++ filter p l, bs.reverse ++ filter (not ∘ p) l) :=
    match l with
    | [] => by simp [partition.loop, filter]
    | a :: l => by cases pa : p a <;> simp [partition.loop, pa, aux, filter, append_assoc]
```

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

TITLE: Example Lean main file
DESCRIPTION: This Lean code imports the `Hello` module and defines the `main` function, which prints "Hello, world!" to the console.

SOURCE: https://github.com/leanprover/lean4/blob/master/src/lake/README.md#_snippet_5

LANGUAGE: lean
CODE:
```
import «Hello»

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

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

TITLE: Multi-line Documentation Comment Example
DESCRIPTION: This example shows the correct style for a multi-line documentation comment in Lean 4, with the delimiters on their own lines and the comment itself unindented.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/style.md#_snippet_13

LANGUAGE: lean
CODE:
```
/--
Monadically computes a value by folding the given function over the mappings in the hash
map in some order.
-/
@[inline] def foldM (f : δ → (a : α) → β a → m δ) (init : δ) (b : Raw α β) : m δ :=
  b.buckets.foldlM (fun acc l => l.foldlM f acc) init
```

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

TITLE: Running the Defined Script
DESCRIPTION: These shell commands demonstrate how to run the `greet` script defined in the `lakefile.lean` file. The first command runs the script without arguments, resulting in "Hello, world!" being printed. The second command runs the script with the argument "me", resulting in "Hello, me!" being printed.

SOURCE: https://github.com/leanprover/lean4/blob/master/src/lake/README.md#_snippet_30

LANGUAGE: shell
CODE:
```
$ lake script run greet
Hello, world!
$ lake script run greet me
Hello, me!
```

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

TITLE: Example Lean library root module
DESCRIPTION: This Lean code imports the `Hello.Basic` module. This module serves as the root of the `Hello` library.

SOURCE: https://github.com/leanprover/lean4/blob/master/src/lake/README.md#_snippet_4

LANGUAGE: lean
CODE:
```
-- This module serves as the root of the `Hello` library.
-- Import modules here that should be built as part of the library.
import «Hello».Basic
```

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

TITLE: Installing meld on Ubuntu
DESCRIPTION: Installs the meld tool, which is used for comparing files, on an Ubuntu system. This is a prerequisite for comparing the produced and expected outputs of Lean4 tests.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/dev/testing.md#_snippet_5

LANGUAGE: bash
CODE:
```
sudo apt-get install meld
```

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

TITLE: Running the Defined Script
DESCRIPTION: These shell commands demonstrate how to run the `greet` script defined in the `lakefile.lean` file. The first command runs the script without any arguments, resulting in a "Hello, world!" message. The second command runs the script with the argument "me", resulting in a "Hello, me!" message.

SOURCE: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md#_snippet_28

LANGUAGE: Shell
CODE:
```
$ lake script run greet
Hello, world!
$ lake script run greet me
Hello, me!
```

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

TITLE: Single-line Documentation Comment Example
DESCRIPTION: This example shows the correct style for a single-line documentation comment in Lean 4, placed on the same line as the `/--` and `-/` delimiters.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/style.md#_snippet_12

LANGUAGE: lean
CODE:
```
/-- Carries out a monadic action on each mapping in the hash map in some order. -/
@[inline] def forM (f : (a : α) → β a → m PUnit) (b : Raw α β) : m PUnit :=
  b.buckets.forM (AssocList.forM f)
```

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

TITLE: Displaying Script Documentation
DESCRIPTION: This shell command shows how to display the docstring associated with the `greet` script using `lake script doc`. The output includes the description, usage instructions, and purpose of the script as defined in the `lakefile.lean` file.

SOURCE: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md#_snippet_29

LANGUAGE: Shell
CODE:
```
$ lake script doc greet
Display a greeting

USAGE:
  lake run greet [name]

Greet the entity with the given name. Otherwise, greet the whole world.
```

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

TITLE: Copy Lean Dependencies
DESCRIPTION: This command copies the necessary DLL files from the MSYS2 environment to the current directory. This allows the Lean executable to run independently of the MSYS2 installation.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/make/msys2.md#_snippet_5

LANGUAGE: bash
CODE:
```
cp $(ldd lean.exe | cut -f3 -d' ' | grep mingw) .
```

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

TITLE: Theorem proving with intro+match syntax sugar
DESCRIPTION: This example demonstrates proving a theorem using the `intro+match` syntax sugar within the tactic DSL. It proves `p ∨ q → q ∨ p` using a more concise syntax for pattern matching after introducing the hypothesis.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/tactics.md#_snippet_2

LANGUAGE: lean
CODE:
```
theorem ex3 : p ∨ q → q ∨ p := by
  intro
  | Or.inl h1 =>
    apply Or.inr
    exact h1
  | Or.inr h2 =>
    apply Or.inl
    assumption
```

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

TITLE: Theorem proving with pattern matching in intro
DESCRIPTION: This example demonstrates using pattern matching within the `intro` tactic. It proves `s ∧ q ∧ r → p ∧ r → q ∧ p` by directly destructuring the input hypotheses.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/tactics.md#_snippet_8

LANGUAGE: lean
CODE:
```
theorem ex1 : s ∧ q ∧ r → p ∧ r → q ∧ p := by
  intro ⟨_, ⟨hq, _⟩⟩ ⟨hp, _⟩
  exact ⟨hq, hp⟩
```

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

TITLE: Defining a Subarray Structure in Lean 4
DESCRIPTION: Defines a structure `Subarray` representing a section of an array that shares the underlying memory allocation. It includes fields for the underlying array (`array`), start index (`start`), and stop index (`stop`). It also includes proofs that the start is less than or equal to the stop and that the stop is within the bounds of the array.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/style.md#_snippet_15

LANGUAGE: Lean
CODE:
```
/--
 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
```

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

TITLE: Testing the Web Server with Netcat
DESCRIPTION: This bash command uses netcat to set up a local port and forward requests to the Lean 4 web server. It allows testing the server in a browser by accessing it at http://localhost:1234.

SOURCE: https://github.com/leanprover/lean4/blob/master/tests/playground/webserver/README.md#_snippet_1

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

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

TITLE: Theorem with Attribute on Same Line
DESCRIPTION: This example demonstrates placing an attribute (`simp`) on the same line as the theorem declaration in Lean 4.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/style.md#_snippet_10

LANGUAGE: lean
CODE:
```
@[simp] theorem eraseP_nil : [].eraseP p = [] := rfl
```

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

TITLE: Basic Parallelized Release Build using CMake
DESCRIPTION: This snippet demonstrates how to clone the Lean 4 repository, navigate to the directory, configure a release build using CMake, and compile the library and binaries in parallel using the `make` command. It uses `nproc` or `sysctl` to determine the number of available processors for parallel compilation.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/make/index.md#_snippet_0

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

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

TITLE: Theorem with decreasing_by and assumption
DESCRIPTION: This example demonstrates a theorem `div_add_mod` with a `decreasing_by` clause that uses `apply div_rec_lemma; assumption` to prove termination.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/style.md#_snippet_17

LANGUAGE: lean
CODE:
```
theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by
  rw [div_eq, mod_eq]
  have h : Decidable (0 < n ∧ n ≤ m) := inferInstance
  cases h with
  | isFalse h => simp [h]
  | isTrue h =>
    simp [h]
    have ih := div_add_mod (m - n) n
    rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2]
decreasing_by apply div_rec_lemma; assumption
```

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

TITLE: Theorem proving using tactics
DESCRIPTION: This example demonstrates proving a theorem using basic tactics like intro, cases, apply, and exact within the tactic DSL. It shows a structured approach to proving `p ∨ q → q ∨ p`.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/tactics.md#_snippet_0

LANGUAGE: lean
CODE:
```
theorem ex1 : p ∨ q → q ∨ p := by
  intro h
  cases h with
  | inl h1 =>
    apply Or.inr
    exact h1
  | inr h2 =>
    apply Or.inl
    assumption
```

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

TITLE: Building the Manual with Nix
DESCRIPTION: This command builds the Lean 4 manual using Nix. It updates the lean input and builds the documentation in the ./doc directory.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/dev/mdbook.md#_snippet_1

LANGUAGE: bash
CODE:
```
nix build --update-input lean ./doc
```

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

TITLE: Theorem with Attribute on Separate Line
DESCRIPTION: This example demonstrates placing an attribute (`simp`) on a separate line before the theorem declaration in Lean 4.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/style.md#_snippet_11

LANGUAGE: lean
CODE:
```
@[simp]
theorem eraseP_nil : [].eraseP p = [] := rfl
```

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

TITLE: Documenting Axiom of Choice in Lean 4
DESCRIPTION: This example demonstrates how to document the Axiom of Choice in Lean 4, including a detailed explanation of its usage and implications for noncomputable definitions.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/style.md#_snippet_3

LANGUAGE: Lean
CODE:
```
/--
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 α → α
```

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

TITLE: Displaying Script Documentation
DESCRIPTION: This shell command shows how to display the docstring associated with the `greet` script using `lake script doc`. The output includes the description, usage instructions, and purpose of the script as defined in the lakefile.lean.

SOURCE: https://github.com/leanprover/lean4/blob/master/src/lake/README.md#_snippet_31

LANGUAGE: shell
CODE:
```
$ lake script doc greet
Display a greeting

USAGE:
  lake run greet [name]

Greet the entity with the given name. Otherwise, greet the whole world.
```

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

TITLE: Building a Lean Package with lake
DESCRIPTION: This command builds the Lean package, typechecking the code and building all dependencies. It uses the lake package manager to compile the project.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/setup.md#_snippet_2

LANGUAGE: sh
CODE:
```
lake build
```

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

TITLE: Theorem with induction and pattern matching
DESCRIPTION: This example shows a theorem `eq_append_cons_of_mem` that uses induction on a `List`. The match arms within the induction step are indented appropriately.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/style.md#_snippet_20

LANGUAGE: lean
CODE:
```
theorem eq_append_cons_of_mem {a : α} {xs : List α} (h : a ∈ xs) :
    ∃ as bs, xs = as ++ a :: bs ∧ a ∉ as := by
  induction xs with
  | nil => cases h
  | cons x xs ih =>
    simp at h
    cases h with
    | inl h => exact ⟨[], xs, by simp_all⟩
    | inr h =>
      by_cases h' : a = x
      · subst h'
        exact ⟨[], xs, by simp⟩
      · obtain ⟨as, bs, rfl, h⟩ := ih h
        exact ⟨x :: as, bs, rfl, by simp_all⟩
```

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

TITLE: Updating and Activating Lean 4 with elan
DESCRIPTION: These commands update elan and then download and activate the latest stable release of Lean 4 using elan. This is the recommended way to manage Lean versions.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/setup.md#_snippet_0

LANGUAGE: sh
CODE:
```
$ elan self update  # in case you haven't updated elan in a while
# download & activate latest Lean 4 stable release (https://github.com/leanprover/lean4/releases)
$ elan default leanprover/lean4:stable
```

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

TITLE: Function definition with pattern matching
DESCRIPTION: This example demonstrates a function `alter` that uses pattern matching on an `AssocList`. The match arms are indented to the same level as the `match` keyword.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/style.md#_snippet_19

LANGUAGE: lean
CODE:
```
def alter [BEq α] {β : Type v} (a : α) (f : Option β → Option β) :
    AssocList α (fun _ => β) → AssocList α (fun _ => β)
  | nil => match f none with
    | none => nil
    | some b => AssocList.cons a b nil
  | cons k v l =>
    if k == a then
      match f v with
      | none => l
      | some b => cons a b l
    else
      cons k v (alter a f l)
```

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

TITLE: Getting Standard Input Stream in Lean
DESCRIPTION: Returns the current thread's standard input stream. Use `IO.setStdin` to replace the current thread's standard input stream.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/style.md#_snippet_10

LANGUAGE: Lean
CODE:
```
/--
Returns the current thread's standard input stream.

Use `IO.setStdin` to replace the current thread's standard input stream.
-/ 
@[extern "lean_get_stdin"] opaque getStdin  : BaseIO FS.Stream
```

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

TITLE: Defining a Script in lakefile.lean
DESCRIPTION: This Lean code defines a script named `greet` within a `lakefile.lean` configuration file. The script takes a list of arguments and prints a greeting, either to a specified name or to the world if no name is provided. It uses the `Lake` and `DSL` modules and returns a `UInt32` exit code.

SOURCE: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md#_snippet_27

LANGUAGE: Lean
CODE:
```
import Lake
open Lake DSL

package scripts

/--
Display a greeting

USAGE:
  lake run greet [name]

Greet the entity with the given name. Otherwise, greet the whole world.
-/
script greet (args) do
  if h : 0 < args.length then
    IO.println s!"Hello, {args[0]'h}!"
  else
    IO.println "Hello, world!"
  return 0
```

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

TITLE: Theorem proving with case tactic and tags
DESCRIPTION: This example demonstrates using the `case` tactic with tags to solve specific subgoals. It proves `p ∨ q → q ∨ p` by explicitly handling each case generated by the `cases` tactic using constructor names as tags.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/tactics.md#_snippet_6

LANGUAGE: lean
CODE:
```
theorem ex4 : p ∨ q → q ∨ p := by
  intro h
  cases h
  case inr =>
    apply Or.inl
    assumption
  case inl =>
    apply Or.inr
    assumption
```

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

TITLE: Structure definition with deriving clause
DESCRIPTION: This example shows how to define a structure `Iterator` with fields `array` and `idx`, and automatically derive the `Inhabited` instance using the `deriving` clause.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/style.md#_snippet_18

LANGUAGE: lean
CODE:
```
structure Iterator where
  array : ByteArray
  idx : Nat
deriving Inhabited
```

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

TITLE: Set Elan Path in MSYS2
DESCRIPTION: This command sets the PATH environment variable to include the elan binaries directory in MSYS2. It ensures that elan commands are accessible from the command line.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/make/msys2.md#_snippet_4

LANGUAGE: bash
CODE:
```
export PATH="$PATH:/c/users/$USERNAME/.elan/bin"
```

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

TITLE: Building the book with mdbook
DESCRIPTION: This command builds the book using mdbook, generating the HTML output in the `out` directory.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/dev/mdbook.md#_snippet_4

LANGUAGE: bash
CODE:
```
cd lean4/doc
mdbook build
```

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

TITLE: Function with pattern matching and Option types
DESCRIPTION: This example demonstrates a function `mkEqTrans?` that uses pattern matching on two `Option Expr` values. The match arms are aligned for readability.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/style.md#_snippet_21

LANGUAGE: lean
CODE:
```
def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) :=
  match h₁?, h₂? with
  | none, none       => return none
  | none, some h     => return h
  | some h, none     => return h
  | some h₁, some h₂ => mkEqTrans h₁ h₂
```

LANGUAGE: lean
CODE:
```
def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) :=
  match h₁?, h₂? with
  | none, none => return none
  | none, some h => return h
  | some h, none => return h
  | some h₁, some h₂ => mkEqTrans h₁ h₂
```

LANGUAGE: lean
CODE:
```
def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) :=
  match h₁?, h₂? with
  | none,    none    => return none
  | none,    some h  => return h
  | some h,  none    => return h
  | some h₁, some h₂ => mkEqTrans h₁ h₂
```

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

TITLE: Executing the Generated Program
DESCRIPTION: This snippet shows how to execute the generated `test` program with command-line arguments. The program is expected to print the arguments as a result.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/examples/compiler/README.md#_snippet_0

LANGUAGE: Shell
CODE:
```
./build/bin/test hello world
```

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

TITLE: Theorem with Equality and Casting in Lean
DESCRIPTION: This Lean code presents a theorem `get?_alter` that includes an equality check and a cast operation. The code is split across multiple lines for clarity.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/std/style.md#_snippet_4

LANGUAGE: lean
CODE:
```
theorem get?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    (m.alter k f).get? k' =
      if h : k == k' then
        cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (m.get? k))
      else m.get? k' := by
 simp_to_raw using Raw₀.get?_alter
```

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

TITLE: Defining a Script in lakefile.lean
DESCRIPTION: This Lean code defines a script named `greet` within a `lakefile.lean` configuration file. The script takes a list of arguments and prints a greeting, either to a specified name or to the world if no name is provided. It uses the `Lake` and `DSL` modules and returns a `UInt32` exit code.

SOURCE: https://github.com/leanprover/lean4/blob/master/src/lake/README.md#_snippet_29

LANGUAGE: lean
CODE:
```
import Lake
open Lake DSL

package scripts

/--
Display a greeting

USAGE:
  lake run greet [name]

Greet the entity with the given name. Otherwise, greet the whole world.
-/
script greet (args) do
  if h : 0 < args.length then
    IO.println s!"Hello, {args[0]'h}!"
  else
    IO.println "Hello, world!"
  return 0
```

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

TITLE: Iterative Computation in Lean
DESCRIPTION: 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.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/style.md#_snippet_11

LANGUAGE: Lean
CODE:
```
/--
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 example
#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
```

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

TITLE: Absolute Declaration Names in Lean 4
DESCRIPTION: This example illustrates how to use absolute names in Lean 4 by starting a declaration name with `_root_`. This allows accessing declarations from the root namespace, even when shadowing occurs in inner namespaces.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/declarations.md#_snippet_1

LANGUAGE: lean
CODE:
```
opaque a : Nat
namespace A
  opaque a : Int
  #print _root_.a -- opaque a : Nat
  #print A.a      -- opaque A.a : Int
end A
```

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

TITLE: Theorem proving with pattern matching and funext
DESCRIPTION: This example demonstrates using pattern matching with `funext` tactic. It proves the equality of two functions by destructuring the input pairs and using `Nat.add_comm`.

SOURCE: https://github.com/leanprover/lean4/blob/master/doc/tactics.md#_snippet_9

LANGUAGE: lean
CODE:
```
theorem ex2 :
    (fun (x : Nat × Nat) (y : Nat × Nat) => x.1 + y.2)
    =
    (fun (x : Nat × Nat) (z : Nat × Nat) => z.2 + x.1) := by
  funext (a, b) (c, d)
  show a + d = d + a
  rw [Nat.add_comm]
```