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)
- Evaluation
- Assignment
- Data Types
  - Structural Types
  - Inductive Types
  - Booleans
  - Numbers
  - Lists
- Classes
- Coersion
- Errors
- [Iteration](#iteration)
- IO
- Monads
- Modules
- Macros
- Proof
  - Dependent Types
  - Tactics

## Documentation

First: where is the documentation?

The primary source of documentation is the [Lean source code documentation](https://leanprover-community.github.io/mathlib4_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, but these docs are as close as it gets.

The secondary source of documentation is the [Lean Zulip](https://leanprover.zulipchat.com/). 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 wonderfully nice and very knowledgeable people: with both channels for 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, [*Theorem Proving in Lean*](https://leanprover.github.io/theorem_proving_in_lean4/introduction.html) or [*Functional Programming in Lean*](https://leanprover.github.io/functional_programming_in_lean/introduction.html) are alternately recommended. There are a good deal more, which I have not read:
- [*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/)

Finally, there is [the Lean manual](https://lean-lang.org/lean4/doc/). It is *very* much a work in progress, and contains plenty of blank pages: but, I've found some sections helpful on occasion.

## 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:
- 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`
  - `macro` `macro_rules` `notation` `syntax`
- 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`
- 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

This list is unlikely to be comprehensive.

The standard data types included in core Lean are the following:
- unit: [`Unit`]
- booleans: [`Bool`]
- numbers: [`Nat`] [`Int`] [`Fin n`]
  - [`USize`] [`UInt8`] [`UInt16`] [`UInt32`] [`UInt64`] [`BitVec`]
- 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`]: 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

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, by the way, 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.)

## Evaluation

## Assignment

## Data Types

### Structural Types

### Inductive Types

### Booleans

### Numbers

### Lists

## Errors

## 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 side effects. And `for`/`while`/`repeat` return only the Unit value, providing no information.

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 use this new `Stream α`.

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

## IO

## Monads

## Modules

## Macros

## Proof