path: root/plt/lean.md

---
layout: plt
title: An Unofficial Lean Reference
---

# imperative programming in lean

[Lean](https://lean-lang.org/) is a combination programming language and theorem prover. It's a pretty neat language!

I found it hard to get started with, however. This guide is an attempt at remedying that.

## table of contents

- [Documentation](#documentation)
- [Prelude](#prelude)
- Basics
- [Assignment](#assignment)
- Functions
- Data Types
  - [Structures](#structures)
  - [Products](#products)
  - Inductives
  - [Sums](#sums)
  - [Booleans](#booleans)
  - [Numbers](#numbers)
  - [Lists](#lists)
  - [Strings](#strings)
- Classes
  - Coersion
- Monads
  - IO
  - Errors
  - [Iteration](#iteration)
- Modules
- Macros
- Proof
  - Dependent Types
  - Tactics

## Documentation

First: where is the documentation?

The primary source of documentation is the [Lean source code documentation][Main Docs]. Despite the URL, it covers more than just mathlib - also generating docs from the (heavily commented) standard library and compiler code base. Lean does not have a comprehensive reference manual, and so these docs are as close as it gets.

The secondary source of documentation is the [Lean Zulip]. Zulip is a tool that is for chat software what Stack Exchange was for forums: it turns them into a searchable, <span title="Though, it doesn't seem to be indexed by Google.">indexable</span> *knowledge database*. The Lean Zulip in particular is host to a wide variety of wonderful and very knowledgeable people: with channels for both compiler development and new-to-Lean questions alike.

There is additionally the [official documentation page](https://lean-lang.org/documentation/) and the [unofficial documentation page](https://leanprover-community.github.io/learn.html), which together catalogue most all of the other learning resources available for Lean.

There are also several books written for Lean. Depending on what you want to do, *[Functional Programming in Lean]* or *[Theorem Proving in Lean]* are alternately recommended. There are a good deal more, which I have not read:
- *[Mathematics in Lean]*
- *[The Mechanics of Proof]*
- *[The Hitchhiker's Guide to Logical Verification]*
- *[Metaprogramming in Lean]*

Finally, there is [the Lean manual][Lean Manual]. It is *very* much a work in progress and contains plenty of blank pages. But, I've found some sections helpful on occasion.

[Main Docs]: https://leanprover-community.github.io/mathlib4_docs/
[Lean Zulip]: https://leanprover.zulipchat.com/
[Theorem Proving in Lean]: https://leanprover.github.io/theorem_proving_in_lean4/introduction.html
[Functional Programming in Lean]: https://leanprover.github.io/functional_programming_in_lean/introduction.html
[Mathematics in Lean]: https://leanprover-community.github.io/mathematics_in_lean/
[The Mechanics of Proof]: https://hrmacbeth.github.io/math2001/
[The Hitchhiker's Guide to Logical Verification]: https://browncs1951x.github.io/static/files/hitchhikersguide.pdf
[Metaprogramming in Lean]: https://leanprover-community.github.io/lean4-metaprogramming-book/
[Lean Manual]: https://lean-lang.org/lean4/doc/

## Prelude

Second: what is *in* the language, really? Is there a syntactic reference?

The short answer is no, there is not a syntax reference, and if there existed one it wouldn't be very helpful. Lean has an extremely powerful metaprogramming system: and the majority of *syntax* in Lean is user-defined.

However. To my best understanding, the syntactic forms are as follows:

<details>
<summary>expand</summary>

- types: `:`
  - [`structure`] [`inductive`] <span title="Coinductive types do not actually exist yet.">`coinductive`</span> [`class`] `instance`
  - `where` `instance` `extends` `deriving`
- values:
  - `""` `''` `«»` `[]` `#[]` `{}` `()` `fun` `λ`
  - `--` `/- -/` `/-- -/` `/-! -/`
  - `×` `⊕`
  - numbers `0b` `0x` ...
- assignment: `:=`
  - `def` `abbrev`
  - `let` `let rec` `let mut`
- control flow: `if`/`then`/`else` `match`/`with`
- iteration:
  - `for`/`in`/`do` `while`/`do` `repeat`
  - `return` `continue` `break`
- exceptions: `try` `catch` `finally`
- monads: `<-` [`do`] (also `failure` `pure`)
- modules:
  - `namespace`/`end` `section`/`end`
  - `open`/`in` `import`
  - `hiding` `renaming` `exposing`
  - `export` `private` `protected` ...
- modifiers: `@[...]` `partial` `noncomputable` `nonrec`
- macros:
  - `macro` `macro_rules` `notation` `syntax`
  - `infix` `infixl` `infixr` `postfix` `prefix`
- debugging: `assert!` `dbg_trace`
- proof:
  - `axiom` `theorem` `lemma`
  - `show` `from` `have` `by` `at` `this`
  - `suffices` `calc` `admit`
- holes: `sorry` `stop`
- evaluation: `#eval` `#check` `#check_failure` `#reduce` `#print`

[`structure`]: https://leanprover.github.io/functional_programming_in_lean/getting-to-know/structures.html
[`inductive`]: https://leanprover.github.io/functional_programming_in_lean/getting-to-know/datatypes-and-patterns.html
[`class`]: https://leanprover.github.io/functional_programming_in_lean/type-classes/polymorphism.html

[`do`]: https://lean-lang.org/lean4/doc/do.html

</details>

This list is unlikely to be comprehensive.

The standard data types included in core Lean are the following:

<details>
<summary>expand</summary>

- unit: [`Unit`]
- booleans: [`Bool`]
- numbers: [`Nat`] [`Int`] [`Fin n`]
  - [`USize`] [`UInt8`] [`UInt16`] [`UInt32`] [`UInt64`] [`BitVec w`]
- strings: [`Char`] [`String`] [`Substring`]
- lists: [`List α`] [`Array α`] [`Subarray`]
  - [`ByteArray`] [`FloatArray`]
  - (see also: [`Batteries.Vector α n`])
- errors: [`Option α`] [`Except ε α`]
- data: [`Prod α β`] [`Sum α β`]
  - (see also: [`structure`] [`inductive`])
- types: [`Empty`] [`Nonempty`] [`Type`/`Prop`/`Type u`/`Sort u`]
- proof:
  - [`And α β`] [`Or α β`] [`Iff α β`] [`True`] [`False`]
  - [`Eq α β`] [`Equivalence`]
  - [`Exists`] (where is `Forall`?)

[`Unit`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Unit
[`Bool`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Bool
[`Nat`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Nat
[`Int`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/Int/Basic.html
[`Fin n`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Fin
[`USize`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#USize
[`UInt8`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt8
[`UInt16`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt16
[`UInt32`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt32
[`UInt64`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt64
[`BitVec w`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/BitVec/Basic.html
[`Char`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Char
[`String`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#String
[`Substring`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Substring
[`List α`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#List
[`Array α`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Array
[`Subarray`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Subarray
[`Batteries.Vector α n`]: https://leanprover-community.github.io/mathlib4_docs/Batteries/Data/Vector/Basic.html
[`ByteArray`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/ByteArray/Basic.html
[`FloatArray`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/FloatArray/Basic.html
[`Option α`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Option
[`Except ε α`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Except
[`Prod α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Prod
[`Sum α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Sum
[`Empty`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Empty
[`Nonempty`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Nonempty
[`Type`/`Prop`/`Type u`/`Sort u`]: https://leanprover-community.github.io/mathlib4_docs/foundational_types.html
[`And α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#And
[`Or α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Or
[`Iff α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Iff
[`True`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#True
[`False`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#False
[`Eq α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Eq
[`Equivalence`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Equivalence
[`Exists`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Exists

</details>


## Basics

Lean is a functional programming language. todo

The best way to find out what you're looking at is to use VS Code's right-click "Go to Declaration" feature. On a type, it'll drop you at its declaration. On a term, it'll drop you on its definition. On a *syntactic element*, it will either drop you into the core Lean codebase, or, more likely, onto a *macro syntax rule*.

(If you are not writing Lean in VS Code, you should be. Lean has *extremely* good tooling that is primarily based around VS Code. Emacs is the only other option but is much less maintained.)

## Assignment

There are several ways to declare variables and functions:
- `def` introduces a *named* definition.
- `let` defines a *local* binding.
  - `let rec` declares a *local recursive* binding.
  - `let mut` defines a *mutable* binding.
- `abbrev` defines a transparent alias.

All of these may take parameters.

```haskell
def hello := "Hello"
def world : String :=
  let world := "world"
  let world := world.push '!'
  world

def inc (n : Nat) : Nat := n + 1
def dec n := n - 1

abbrev Byte := UInt8
```

The walrus operator `:=` is used for assignment, as `=` is used for *querying* equality. It follows the name of a `def`, `let`, or `abbrev` declaration. A type annotation can optionally precede `:=`. In most cases, they are not necessary - Lean has good type inference. The `←` operator is occasionally also used for assignment, in a similar fashion to `:=`. Its semantics are complex and covered in the section on monads.

The primary distinction between `def` and `let` is that `let` allows *shadowing*: a future invocation of `let` may overwrite previous `let` bindings. `let` is thus useful for variables, while `def` is more useful for constants and functions that may be exported. `def` is additionally self-referential by default, though there are some asterisks, while `let` requires the use of `let rec`. The `let mut` declaration, it should be noted, is syntactic sugar over the State monad, which we will discuss later.

The `abbrev` declaration creates a direct alias between the left and right hand sides of the declaration. Lean will gratuitously unfold these during overload resolution or when reducing or querying equality.

All definitions may only be used after their declaration. A function thus cannot refer to a function declared after it, nor a structure to a not-yet declared structure. This prevents the declaration of mutually-entangled structures (and functions) and simplifies analysis.

See also: [FPIL:Functions and Definitions](https://leanprover.github.io/functional_programming_in_lean/getting-to-know/functions-and-definitions.html)

## Functions

## Data Types

### Structures

The `structure` type is analogous to structs in other languages. It behaves much as one would expect.

```haskell
structure Header where
  (width height : Nat)
  alpha : Bool
  linear := false

let header : Header := {
  width := 1920
  height := 1080
  alpha := true
}
```

Structures may be declared with the `structure ... where` syntax. Just like functions, multiple fields of the same type may be grouped together, and default values are supported. An individual field with a default value may be omitted in the constructor. A field of a function may or may not be wrapped in parentheses, but parentheses are required for multiple fields of the same type.

Structures may be constructed with braces. The braces are syntactic sugar for an underlying `Name.mk` constructor. Their fields take the form `field := value`, separated either by newlines or by commas. If `value` is a variable of the same name as `field`, the `field :=` portion may be omitted. The brace constructors are *structural*: the order in which fields are declared does not matter, only their name does.

```haskell
def increment_height (header : Header) : Header :=
  let {width, height, alpha, linear} := header
  let height := height + 1
  {width, height, alpha, linear}
```

Structures may be destructured either by pattern matching or with dot notation for field access. Pattern matching may be done via `match` or inline via `let` with the `{}` syntax.

They cannot be mutated: Lean is functional and so there is no explicit syntax for updating a field. `header.width ← ...` does nothing, even if `header` is declared to be mutable. Instead, the entire `header` structure must be updated at once. This can be a pain on large structures, so Lean provides the `with` keyword for succiently (re-)constructing a structure with only a few fields changed. The `increment_height` function above can thus be compactly declared as the following:
```haskell
def increment_height (header : Header) : Header :=
  { header with height := header.height + 1 }
```

Structures may *extend* one another. A structure inherits all the fields of the structures it extends (which must not conflict), and can declare new fields. Default values may be redefined but fields may not be. As a type may not be referenced before its declaration, cyclic extensions cannot be formed.
```haskell
structure Point where
  (x y : Int)

structure Color where
  (r g b a : UInt8)

structure Pixel extends Point, Color

let pixel : Pixel := {
  x := 2000, y := 1000
  r := 255, g := 255, b := 255, a := 255
}
```

Structures may also parametrize over terms or other types. todo

Be warned - the `where` in a `structure` declaration is mandatory. Leaving off the `where` will result in a (valid!) structure with *zero* fields, that is instead *parametrized* over what were intended to be the fields. This can lead to strange type errors.

See also: [FPIL:Structures](https://leanprover.github.io/functional_programming_in_lean/getting-to-know/structures.html), [FPIL:Structures and Inheritance](https://leanprover.github.io/functional_programming_in_lean/functor-applicative-monad/inheritance.html), [Manual:Structures](https://lean-lang.org/lean4/doc/struct.html)

### Products

Sometimes, it is convenient to not need to bother with naming structures or their fields. Whether inline within the definition of a more complex type, or as the return type of a helper function, it can be the case that having explicit names is more trouble than it is worth.

Lean provides a type for *anonymous structures*, that behave in a very similar fashion to *tuples* in other languages. This is called `Prod` on analogy with `Sum` (which we will see later).
```haskell
structure Prod (α : Type) (β : Type) where
  fst : α
  snd : β

abbrev Image := (Header × Array Pixel)
let image : Image := (header, #[])

#check (image.fst : Header)
```

Lean also provides the compact `α × β` notation as syntactic sugar for `Prod α β`. With Lean's rules around function application, tuples of arbitrary arity can be written `α × β × γ × ...`, which is equivalent to `α × (β × (γ × ...))` (and `Prod α Prod β Prod γ ...`).

While products can be constructed with `Prod.mk a b` or `{ fst := a, snd := b }`, there is also tuple-like notation for constructing them: `(a, b, ...)`. This is overloaded to function for products of arbitrary arity. Similar to tuples elsewhere, the `.fst` and `.snd` destructors have aliases to `.1` and `.2`, respectively - however, there do not exist aliases for the rest of the natural numbers.

The name `Prod` comes from type theory (and category theory more broadly). Structures are a special case of what is more generally called a "product": a vast generalization of the idea of taking a "pair" of something. The design of the `Prod` type aligns significantly closer to the specific formal notion of a "product type" in type theory than `structure` does, making it additionally quite useful for mathematicians.

See also: [FPIL:Polymorphism#Prod](https://leanprover.github.io/functional_programming_in_lean/getting-to-know/polymorphism.html#prod)

### Inductives

### Sums

Similarly to [products](#products), it is sometimes convenient to not need to bother with naming inductives or their variants. The `Sum` type provides for this.
```haskell
inductive Sum (α : Type) (β : Type) where
  | inl (val : α)
  | inr (val : β)
```

Lean provides the compact `α ⊕ β` notation as syntactic sugar for `Sum α β`. This generalizes to sums of arbitrary length: `α ⊕ β ⊕ γ ⊕ ...`. There is no syntactic sugar for `Sum.inl` and `Sum.inr`: sums must be explicitly constructed. There is also no syntactic sugar for destructuring: `match` must be used.

See also: [FPIL/Polymorphism#Sum](https://lean-lang.org/functional_programming_in_lean/getting-to-know/polymorphism.html#sum)

### Booleans

Lean provides a `Bool` type, defined as an inductive data type:
```haskell
inductive Bool where
  | false
  | true
```

The `true` and `false` terms are exported in the Prelude and do not need to be prefixed with `Bool`. Standard `if`/`else` destructors are also provided. `else if` is special cased in the parser to behave nicely.

`if` is also overloaded to function with `let` to provide a compact alternative to a `match` statement.
```haskell
let a := Chunk.rgb 1 2 3
if let {r, g, b} := a then
  IO.println s!"red: {r}, green: {g}, blue: {b}"
```

### Numbers

Lean provides a variety of representations of numbers. The main three are [`Nat`], [`Int`], & [`Fin`][`Fin n`].

[`Nat`] is an arbitrary-sized number type. It is defined as the following:
```haskell
-- Zero is a natural number.
-- The successor of a natural number is a natural number.
inductive Nat where
  | zero
  | succ (n : Nat)
```

Lean recognizes numeric literals (`0`, `1`, `2`...) as numeric constructors, equivalent to their `Nat.succ (Nat.succ ...)` counterparts. Special compiler support allows for representing `Nats` in a reasonable / efficient fashion: numbers smaller than `2^63` are stored directly, while numbers larger than `2^63 - 1` use an [arbitrary precision BigInt library](https://gmplib.org/manual/).

It should be noted that Lean treats operations on `Nat` that would produce a negative number **as producing zero**. For example, `#check 4 - 5` prints `4 - 5 : Nat`, and `#eval 4 - 5` prints `0`.

[`Int`] is an extension of `Nat` to also represent negative numbers. It is similarly special-cased by the compiler. Lean recognizes (..., `-2`, `-1`) as equivalent to their `Int.negSucc n` counterparts, and will also implicitly cast (`0`, `1`, `2`...) to `Int` as required.
```haskell
-- A natural number is an integer.
-- The negation of the *successor* of a natural number is an integer.
-- (the above is enforced by compiler magic)
inductive Int where
  | ofNat (n : Nat)   -- [0 : ∞)
  | negSucc (n : Nat) -- (-∞ : -1]
```

[`Fin n`] is a natural number guaranteed to be *smaller* than `n`. The underlying representation is `val : Nat` and a proof that `val < n`.
```haskell
-- If i : Fin n, then i.val : Nat is the described number.
-- It can also be written as i.1 or just i when the target type is known.
-- If i : Fin n, then i.isLt is a proof that i.val < n.
structure Fin (n : Nat) where
  val  : Nat
  isLt : LT.lt val n
```

Lean supports the following fixed-width integers: [`UInt8`], [`UInt16`], [`UInt32`], [`UInt64`], [`USize`]. They behave as one would expect. `USize` takes the size of a pointer on its appropriate platforms. Lean also supports *arbitrary* fixed-width integers with [`BitVec w`]. They are treated internally as `Fin (2 ^ w)`, and gain all the special support for math that `Fin n` and subsequently `Nat` has.

Lean is good at typechecking numbers. For example, the following code compiles:
```haskell
abbrev UInt6 := BitVec 6
structure Pixel where
  (r g b a : UInt8)

def hash (pixel : Pixel) : UInt6 :=
  -- Lean recognizes the resulting value cannot be larger than 2^6 - 1 or 6 bits, via % 64.
  (pixel.r.val * 3 + pixel.g.val * 5 + pixel.b.val * 7 + pixel.a.val * 11) % 64
```

The expected basic mathematical operations are defined on all numbers. Their semantics differ depending on the specific numeric type.
- arithmetic: `+`, `-`, `*`, `/`, `%`, `∣`
- comparison: `<`, `>`, `<=` and `≤`, `>=` and `≥`
- bitwise: `&&&`, `|||`, `^^^`, `~~~`
- shifts: `<<<`, `>>>`

Numbers regularly need to be explicitly converted between different representations. This may be done via various `.toType` and `.ofType` methods. More on conversion can be found in the Classes section.

See also: [Manual:Naturals](https://lean-lang.org/lean4/doc/nat.html)

### Lists

Lean provides for several representations of list-like data structures.

[`List α`] is the standard representation. It is represented as a linked list, and defined as follows:
```haskell
inductive List (α : Type u) where
  | nil
  | cons (head : α) (tail : List α)
```

`List.nil` or more commonly `[]` represents the empty list. `List.cons a l` or `a :: l` (for some `a : α`, `l : List α`) are used for list concatenation. `[a, b, c, ...]` syntax can also be used for construction of lists. Various functions and classes are defined for and on lists.

[`Array α`] is isomorphic to `List α`. It is represented as a dynamic array. Arrays are significantly more performant than Lists: not only are they more efficient at everything except insertation and deletion, but so long as arrays are used "linearly", Lean will optimize all updates to be *destructive* - which provides comparable performance to mutable arrays in imperative programming languages. As such, **you usually want to use `Array`**.

However: currently `Arrays` are always represented as an array of *pointers* in memory, for ABI reasons. This is an obvious performance pitfall for small types and liable to change in the (near) future. But for now, Lean provides special [`ByteArray`] / [`FloatArray`] types that are treated like `Array UInt8` and `Array Float` respectively, but represented as real unboxed byte/float arrays.

`Array` has different syntax for its constructor: `#[a, b, c]`. It also does not implement `List.cons a l` or `a :: l`. Instead, it uses `Array.push l a`, with elements added to the *end* of the array.

The [`Batteries.Vector α n`] type is not in `Std`, but worth a mention. It is a *statically sized array*: represented under the hood by `Array`, but guaranteed to not change size throughout its existence. It behaves much the same as `Array`, though without `push`.

All lists provide some postfix `list[i]` syntax for accessing arbitrary array elements.
- `list[i]` takes an `i : Fin n`, for `n < list.size`. If this cannot be proven it fails to compile.
- `list[i]?` returns an `Option α`.
- `list[i]!` returns an `α` or panics.

See also: [FPIL:Polymorphism#Linked Lists](https://lean-lang.org/functional_programming_in_lean/getting-to-know/polymorphism.html#linked-lists), [Manual:Arrays](https://lean-lang.org/lean4/doc/array.html)

### Strings

The [`String`] type represents a UTF-8 encoded string. It is treated as a `List Char`, but represented as a packed `ByteArray`. Strings are constructed via `""`.

The [`Char`] type represents a "Unicode scalar value": that is, a codepoint. The underlying value is represented (presumably) in UTF-32 as a `UInt32`. Chars are constructed via `''`. They are ordered, and can be compared using `=`, `<`, `≤`, `>`, and `≥`.

String manipulation can be inefficient. The [`Substring`] type provides an immutable *view* into some subslice of a `String`.

## Classes

### Coersion


## Monads

The [Functional Programming in Lean] book contains extensive information on monads in Lean: [FPIL:Monads](https://leanprover.github.io/functional_programming_in_lean/monads.html), [FPIL:Functors, Applicative Functors, and Monads](https://leanprover.github.io/functional_programming_in_lean/functor-applicative-monad.html), [FPIL:Monad Transformers](https://leanprover.github.io/functional_programming_in_lean/monad-transformers.html).

Those interested in theory and the intricate details may look there. I intend to present a purely-workable overview of the language features implemented *atop* monads.

### IO

### Errors

Lean encodes errors as monads. The [`Option α`] type is by far the most used.

An `Option α` is the following type:
```haskell
inductive Option (α : Type) where
  | none
  | some (val : α)
```

There are other forms of errors. The [`Except ε α`] type allows for encoding a specific error type:
```haskell
inductive Except (ε : Type) (α : Type) where
  | error (err : ε)
  | ok (val : α)
```

### Iteration

Lean has three main syntactic constructs for iteration: `for`, `while`, and `repeat`. They all function pretty much as you would expect and ultimately desugar to lambdas and (tail) recursion.

However: Lean is a purely functional language, as much as it does a good job at hiding it. In the default (pure) context, variable mutation is not allowed. Neither is IO, nor any sort of other side effects. And `for`/`while`/`repeat` may only return the Unit value.

Iteration is thus *useless* in the pure context! We can iterate, for sure, but there may never be any *observable* changes. As such, Lean does not allow `for`/`while`/`repeat` within pure functions. This can be the cause of some strange type errors. Ensure you are only iterating in a monadic `do` context.

(It should be noted that the `do` in `for/in/do` and `while/do` are part of their declaration syntax, and are unrelated to the `do` keyword. Morally, they're the same `do`, though.)

#### implementing iterators: `ForIn` and `Stream`

`for` desugars to an appliction of the `ForIn.forIn` method, so that data structures can implement individually what exactly iteration means for them.

The iteration implemented by `ForIn` is called "internal iteration", which means it is a higher order function where you give the body of the loop to it to run on the elements yielded by the iterator in order. This is in contrast to "external iteration" (in the style of ex. Rust), where the iterator has a function returning the next value of the iterator.

One reason to prefer internal iteration is that it is easier to verify termination. This is something Lean cares very much about. But, internal iteration is a less flexible model than external iteration. You can't quite just convert an internal iterator to an external iterator. So there are some downsides.

Lean also has an external iteration typeclass, called `Stream`, but it is not used as much. `Stream α` provides a `.next?` method that returns an `Option (α × Stream α)`. However, because Lean is purely functional, the burden is on the user to shadow bindings and use this new `Stream α`.

It is probably possible to do external iteration via the State monad. I would like to try this out.

## Modules

## Macros

The standard reference is [Metaprogramming in Lean](https://leanprover-community.github.io/lean4-metaprogramming-book/).

## Proof

The standard reference for type theorists is [Theorem Proving in Lean].

The standard reference for mathematicians is [Mathematics in Lean].

A guide for those new to mathematics entirely is [The Mechanics of Proof].