Store a value in a thunk. Note that the value has already been computed, so there is no laziness.

## Equations

- Thunk.pure a = { fn := fun x => a }

- intro :: (
Modus ponens for if and only if. If

`a ↔ b`

and`a`

, then`b`

.mp : a → bModus ponens for if and only if, reversed. If

`a ↔ b`

and`b`

, then`a`

.mpr : b → a- )

If and only if, or logical bi-implication. `a ↔ b`

means that `a`

implies `b`

and vice versa.
By `propext`

, this implies that `a`

and `b`

are equal and hence any expression involving `a`

is equivalent to the corresponding expression with `b`

instead.

## Instances For

If and only if, or logical bi-implication. `a ↔ b`

means that `a`

implies `b`

and vice versa.
By `propext`

, this implies that `a`

and `b`

are equal and hence any expression involving `a`

is equivalent to the corresponding expression with `b`

instead.

## Equations

- «term_<->_» = Lean.ParserDescr.trailingNode `term_<->_ 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <-> ") (Lean.ParserDescr.cat `term 21))

If and only if, or logical bi-implication. `a ↔ b`

means that `a`

implies `b`

and vice versa.
By `propext`

, this implies that `a`

and `b`

are equal and hence any expression involving `a`

is equivalent to the corresponding expression with `b`

instead.

## Equations

- «term_↔_» = Lean.ParserDescr.trailingNode `term_↔_ 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↔ ") (Lean.ParserDescr.cat `term 21))

- inl: {α : Type u} → {β : Type v} → α → α ⊕ β
Left injection into the sum type

`α ⊕ β`

. If`a : α`

then`.inl a : α ⊕ β`

. - inr: {α : Type u} → {β : Type v} → β → α ⊕ β
Right injection into the sum type

`α ⊕ β`

. If`b : β`

then`.inr b : α ⊕ β`

.

`Sum α β`

, or `α ⊕ β`

, is the disjoint union of types `α`

and `β`

.
An element of `α ⊕ β`

is either of the form `.inl a`

where `a : α`

,
or `.inr b`

where `b : β`

.

## Instances For

`Sum α β`

, or `α ⊕ β`

, is the disjoint union of types `α`

and `β`

.
An element of `α ⊕ β`

is either of the form `.inl a`

where `a : α`

,
or `.inr b`

where `b : β`

.

## Equations

- «term_⊕_» = Lean.ParserDescr.trailingNode `term_⊕_ 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ ") (Lean.ParserDescr.cat `term 30))

- inl: {α : Sort u} → {β : Sort v} → α → α ⊕' β
Left injection into the sum type

`α ⊕' β`

. If`a : α`

then`.inl a : α ⊕' β`

. - inr: {α : Sort u} → {β : Sort v} → β → α ⊕' β
Right injection into the sum type

`α ⊕' β`

. If`b : β`

then`.inr b : α ⊕' β`

.

`PSum α β`

, or `α ⊕' β`

, is the disjoint union of types `α`

and `β`

.
It differs from `α ⊕ β`

in that it allows `α`

and `β`

to have arbitrary sorts
`Sort u`

and `Sort v`

, instead of restricting to `Type u`

and `Type v`

. This means
that it can be used in situations where one side is a proposition, like `True ⊕' Nat`

.

The reason this is not the default is that this type lives in the universe `Sort (max 1 u v)`

,
which can cause problems for universe level unification,
because the equation `max 1 u v = ?u + 1`

has no solution in level arithmetic.
`PSum`

is usually only used in automation that constructs sums of arbitrary types.

## Instances For

`PSum α β`

, or `α ⊕' β`

, is the disjoint union of types `α`

and `β`

.
It differs from `α ⊕ β`

in that it allows `α`

and `β`

to have arbitrary sorts
`Sort u`

and `Sort v`

, instead of restricting to `Type u`

and `Type v`

. This means
that it can be used in situations where one side is a proposition, like `True ⊕' Nat`

.

The reason this is not the default is that this type lives in the universe `Sort (max 1 u v)`

,
which can cause problems for universe level unification,
because the equation `max 1 u v = ?u + 1`

has no solution in level arithmetic.
`PSum`

is usually only used in automation that constructs sums of arbitrary types.

## Equations

- «term_⊕'_» = Lean.ParserDescr.trailingNode `term_⊕'_ 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕' ") (Lean.ParserDescr.cat `term 30))

The first component of a dependent pair. If

`p : @Sigma α β`

then`p.1 : α`

.fst : αThe second component of a dependent pair. If

`p : Sigma β`

then`p.2 : β p.1`

.snd : β fst

`Sigma β`

, also denoted `Σ a : α, β a`

or `(a : α) × β a`

, is the type of dependent pairs
whose first component is `a : α`

and whose second component is `b : β a`

(so the type of the second component can depend on the value of the first component).
It is sometimes known as the dependent sum type, since it is the type level version
of an indexed summation.

## Instances For

The first component of a dependent pair. If

`p : @Sigma α β`

then`p.1 : α`

.fst : αThe second component of a dependent pair. If

`p : Sigma β`

then`p.2 : β p.1`

.snd : β fst

`PSigma β`

, also denoted `Σ' a : α, β a`

or `(a : α) ×' β a`

, is the type of dependent pairs
whose first component is `a : α`

and whose second component is `b : β a`

(so the type of the second component can depend on the value of the first component).
It differs from `Σ a : α, β a`

in that it allows `α`

and `β`

to have arbitrary sorts
`Sort u`

and `Sort v`

, instead of restricting to `Type u`

and `Type v`

. This means
that it can be used in situations where one side is a proposition, like `(p : Nat) ×' p = p`

.

The reason this is not the default is that this type lives in the universe `Sort (max 1 u v)`

,
which can cause problems for universe level unification,
because the equation `max 1 u v = ?u + 1`

has no solution in level arithmetic.
`PSigma`

is usually only used in automation that constructs pairs of arbitrary types.

## Instances For

- intro: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
Existential introduction. If

`a : α`

and`h : p a`

, then`⟨a, h⟩`

is a proof that`∃ x : α, p x`

.

Existential quantification. If `p : α → Prop`

is a predicate, then `∃ x : α, p x`

asserts that there is some `x`

of type `α`

such that `p x`

holds.
To create an existential proof, use the `exists`

tactic,
or the anonymous constructor notation `⟨x, h⟩`

.
To unpack an existential, use `cases h`

where `h`

is a proof of `∃ x : α, p x`

,
or `let ⟨x, hx⟩ := h`

where `.

Because Lean has proof irrelevance, any two proofs of an existential are definitionally equal. One consequence of this is that it is impossible to recover the witness of an existential from the mere fact of its existence. For example, the following does not compile:

```
example (h : ∃ x : Nat, x = x) : Nat :=
let ⟨x, _⟩ := h -- fail, because the goal is `Nat : Type`
x
```

The error message `recursor 'Exists.casesOn' can only eliminate into Prop`

means
that this only works when the current goal is another proposition:

```
example (h : ∃ x : Nat, x = x) : True :=
let ⟨x, _⟩ := h -- ok, because the goal is `True : Prop`
trivial
```

## Instances For

- done: {α : Type u} → α → ForInStep α
`.done a`

means that we should early-exit the loop.`.done`

is produced by calls to`break`

or`return`

in the loop. - yield: {α : Type u} → α → ForInStep α
`.yield a`

means that we should continue the loop.`.yield`

is produced by`continue`

and reaching the bottom of the loop body.

Auxiliary type used to compile `for x in xs`

notation.

This is the return value of the body of a `ForIn`

call,
representing the body of a for loop. It can be:

`.yield (a : α)`

, meaning that we should continue the loop and`a`

is the new state.`.yield`

is produced by`continue`

and reaching the bottom of the loop body.`.done (a : α)`

, meaning that we should early-exit the loop with state`a`

.`.done`

is produced by calls to`break`

or`return`

in the loop,

## Instances For

## Equations

- instInhabitedForInStep = { default := ForInStep.done default }

`forIn x b f : m β`

runs a for-loop in the monad`m`

with additional state`β`

. This traverses over the "contents" of`x`

, and passes the elements`a : α`

to`f : α → β → m (ForInStep β)`

.`b : β`

is the initial state, and the return value of`f`

is the new state as well as a directive`.done`

or`.yield`

which indicates whether to abort early or continue iteration.The expression

`let mut b := ... for x in xs do b ← foo x b`

in a

`do`

block is syntactic sugar for:`let b := ... let b ← forIn xs b (fun x b => do let b ← foo x b return .yield b)`

(Here

`b`

corresponds to the variables mutated in the loop.)

`ForIn m ρ α`

is the typeclass which supports `for x in xs`

notation.
Here `xs : ρ`

is the type of the collection to iterate over, `x : α`

is the element type which is made available inside the loop, and `m`

is the monad
for the encompassing `do`

block.

## Instances

`forIn' x b f : m β`

runs a for-loop in the monad`m`

with additional state`β`

. This traverses over the "contents" of`x`

, and passes the elements`a : α`

along with a proof that`a ∈ x`

to`f : (a : α) → a ∈ x → β → m (ForInStep β)`

.`b : β`

is the initial state, and the return value of`f`

is the new state as well as a directive`.done`

or`.yield`

which indicates whether to abort early or continue iteration.

`ForIn' m ρ α d`

is a variation on the `ForIn m ρ α`

typeclass which supports the
`for h : x in xs`

notation. It is the same as `for x in xs`

except that `h : x ∈ xs`

is provided as an additional argument to the body of the for-loop.

## Instances

- pure: {α β σ : Type u} → α → σ → DoResultPRBC α β σ
`pure (a : α) s`

means that the block exited normally with return value`a`

- return: {α β σ : Type u} → β → σ → DoResultPRBC α β σ
`return (b : β) s`

means that the block exited via a`return b`

early-exit command - break: {α β σ : Type u} → σ → DoResultPRBC α β σ
`break s`

means that`break`

was called, meaning that we should exit from the containing loop - continue: {α β σ : Type u} → σ → DoResultPRBC α β σ
`continue s`

means that`continue`

was called, meaning that we should continue to the next iteration of the containing loop

Auxiliary type used to compile `do`

notation. It is used when compiling a do block
nested inside a combinator like `tryCatch`

. It encodes the possible ways the
block can exit:

`pure (a : α) s`

means that the block exited normally with return value`a`

.`return (b : β) s`

means that the block exited via a`return b`

early-exit command.`break s`

means that`break`

was called, meaning that we should exit from the containing loop.`continue s`

means that`continue`

was called, meaning that we should continue to the next iteration of the containing loop.

All cases return a value `s : σ`

which bundles all the mutable variables of the do-block.

## Instances For

- pure: {α β σ : Type u} → α → σ → DoResultPR α β σ
`pure (a : α) s`

means that the block exited normally with return value`a`

- return: {α β σ : Type u} → β → σ → DoResultPR α β σ
`return (b : β) s`

means that the block exited via a`return b`

early-exit command

Auxiliary type used to compile `do`

notation. It is the same as
`DoResultPRBC α β σ`

except that `break`

and `continue`

are not available
because we are not in a loop context.

## Instances For

- break: {σ : Type u} → σ → DoResultBC σ
`break s`

means that`break`

was called, meaning that we should exit from the containing loop - continue: {σ : Type u} → σ → DoResultBC σ
`continue s`

means that`continue`

was called, meaning that we should continue to the next iteration of the containing loop

Auxiliary type used to compile `do`

notation. It is an optimization of
`DoResultPRBC PEmpty PEmpty σ`

to remove the impossible cases,
used when neither `pure`

nor `return`

are possible exit paths.

## Instances For

- pureReturn: {α σ : Type u} → α → σ → DoResultSBC α σ
This encodes either

`pure (a : α)`

or`return (a : α)`

:`pure (a : α) s`

means that the block exited normally with return value`a`

`return (b : β) s`

means that the block exited via a`return b`

early-exit command

The one that is actually encoded depends on the context of use.

- break: {α σ : Type u} → σ → DoResultSBC α σ
`break s`

means that`break`

was called, meaning that we should exit from the containing loop - continue: {α σ : Type u} → σ → DoResultSBC α σ
`continue s`

means that`continue`

was called, meaning that we should continue to the next iteration of the containing loop

Auxiliary type used to compile `do`

notation. It is an optimization of
either `DoResultPRBC α PEmpty σ`

or `DoResultPRBC PEmpty α σ`

to remove the
impossible case, used when either `pure`

or `return`

is never used.

## Instances For

`x ≈ y`

says that `x`

and `y`

are equivalent. Because this is a typeclass,
the notion of equivalence is type-dependent.

## Equations

- «term_≈_» = Lean.ParserDescr.trailingNode `term_≈_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≈ ") (Lean.ParserDescr.cat `term 51))

`∅`

or`{}`

is the empty set or empty collection. It is supported by the`EmptyCollection`

typeclass.emptyCollection : α

`EmptyCollection α`

is the typeclass which supports the notation `∅`

, also written as `{}`

.

## Instances

`∅`

or `{}`

is the empty set or empty collection.
It is supported by the `EmptyCollection`

typeclass.

## Equations

- «term{}» = Lean.ParserDescr.node `term{} 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "{") (Lean.ParserDescr.symbol "}"))

`∅`

or `{}`

is the empty set or empty collection.
It is supported by the `EmptyCollection`

typeclass.

## Equations

- «term∅» = Lean.ParserDescr.node `term∅ 1024 (Lean.ParserDescr.symbol "∅")

- pure :: (
If

`task : Task α`

then`task.get : α`

blocks the current thread until the value is available, and then returns the result of the task.get : α- )

`Task α`

is a primitive for asynchronous computation.
It represents a computation that will resolve to a value of type `α`

,
possibly being computed on another thread. This is similar to `Future`

in Scala,
`Promise`

in Javascript, and `JoinHandle`

in Rust.

The tasks have an overridden representation in the runtime.

## Instances For

## Equations

Task priority. Tasks with higher priority will always be scheduled before ones with lower priority.

## Equations

The default priority for spawned tasks, also the lowest priority: `0`

.

## Equations

The highest regular priority for spawned tasks: `8`

.

Spawning a task with a priority higher than `Task.Priority.max`

is not an error but
will spawn a dedicated worker for the task, see `Task.Priority.dedicated`

.
Regular priority tasks are placed in a thread pool and worked on according to the priority order.

## Equations

Any priority higher than `Task.Priority.max`

will result in the task being scheduled
immediately on a dedicated thread. This is particularly useful for long-running and/or
I/O-bound tasks since Lean will by default allocate no more non-dedicated workers
than the number of cores to reduce context switches.

## Equations

`spawn fn : Task α`

constructs and immediately launches a new task for
evaluating the function `fn () : α`

asynchronously.

`prio`

, if provided, is the priority of the task.

## Equations

- Task.spawn fn prio = { get := fn () }

`map f x`

maps function `f`

over the task `x`

: that is, it constructs
(and immediately launches) a new task which will wait for the value of `x`

to
be available and then calls `f`

on the result.

`prio`

, if provided, is the priority of the task.

`bind x f`

does a monad "bind" operation on the task `x`

with function `f`

:
that is, it constructs (and immediately launches) a new task which will wait
for the value of `x`

to be available and then calls `f`

on the result,
resulting in a new task which is then run for a result.

`prio`

, if provided, is the priority of the task.

You should not use this function

val : Nat

`NonScalar`

is a type that is not a scalar value in our runtime.
It is used as a stand-in for an arbitrary boxed value to avoid excessive
monomorphization, and it is only created using `unsafeCast`

. It is somewhat
analogous to C `void*`

in usage, but the type itself is not special.

## Instances For

- mk: Nat → PNonScalar
You should not use this function

`PNonScalar`

is a type that is not a scalar value in our runtime.
It is used as a stand-in for an arbitrary boxed value to avoid excessive
monomorphization, and it is only created using `unsafeCast`

. It is somewhat
analogous to C `void*`

in usage, but the type itself is not special.

This is the universe-polymorphic version of `PNonScalar`

; it is preferred to use
`NonScalar`

instead where applicable.

## Instances For

# Boolean operators #

`x != y`

is boolean not-equal. It is the negation of `x == y`

which is supplied by
the `BEq`

typeclass.

Unlike `x ≠ y`

(which is notation for `Ne x y`

), this is `Bool`

valued instead of
`Prop`

valued. It is mainly intended for programming applications.

## Equations

- «term_!=_» = Lean.ParserDescr.trailingNode `term_!=_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " != ") (Lean.ParserDescr.cat `term 51))

If

`a == b`

evaluates to`true`

, then`a`

and`b`

are equal in the logic.`==`

is reflexive, that is,`(a == a) = true`

.

`LawfulBEq α`

is a typeclass which asserts that the `BEq α`

implementation
(which supplies the `a == b`

notation) coincides with logical equality `a = b`

.
In other words, `a == b`

implies `a = b`

, and `a == a`

is true.

## Instances

# Logical connectives and equality #

`True`

is true, and `True.intro`

(or more commonly, `trivial`

)
is the proof.

## Equations

`a ≠ b`

, or `Ne a b`

is defined as `¬ (a = b)`

or `a = b → False`

,
and asserts that `a`

and `b`

are not equal.

## Equations

- «term_≠_» = Lean.ParserDescr.trailingNode `term_≠_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≠ ") (Lean.ParserDescr.cat `term 51))

# Exists #

# Decidable #

Synonym for `dite`

(dependent if-then-else). We can construct an element `q`

(of any sort, not just a proposition) by cases on whether `p`

is true or false,
provided `p`

is decidable.

## Equations

- Decidable.byCases h1 h2 = match dec with | isTrue h => h1 h | isFalse h => h2 h

Transfer a decidability proof across an equality of propositions.

## Equations

- decidable_of_decidable_of_eq h = decidable_of_decidable_of_iff (_ : p ↔ q)

## Equations

- instDecidableForAll = if hp : p then if hq : q then isTrue (instDecidableForAll.proof_1 hq) else isFalse (_ : (p → q) → False) else isTrue (instDecidableForAll.proof_3 hp)

# if-then-else expression theorems #

Auxiliary definition for generating compact `noConfusion`

for enumeration types

## Equations

- noConfusionTypeEnum f P x y = Decidable.casesOn (inst (f x) (f y)) (fun x => P) fun x => P → P

Auxiliary definition for generating compact `noConfusion`

for enumeration types

## Equations

- noConfusionEnum f h = Decidable.casesOn (inst (f x) (f y)) (fun h' => False.elim (_ : False)) fun x x => x

# Inhabited #

## Equations

- instInhabitedForInStep_1 = { default := ForInStep.done default }

## Equations

- instInhabitedTrue = { default := True.intro }

## Equations

- instInhabitedPNonScalar = { default := PNonScalar.mk default }

## Equations

- instInhabitedNonScalar = { default := { val := default } }

# Subsingleton #

- intro :: (
Any two elements of a subsingleton are equal.

allEq : ∀ (a b : α), a = b- )

A "subsingleton" is a type with at most one element.
In other words, it is either empty, or has a unique element.
All propositions are subsingletons because of proof irrelevance, but some other types
are subsingletons as well and they inherit many of the same properties as propositions.
`Subsingleton α`

is a typeclass, so it is usually used as an implicit argument and
inferred by typeclass inference.

## Instances

## Equations

An equivalence relation is reflexive:

`x ~ x`

refl : (x : α) → r x xAn equivalence relation is symmetric:

`x ~ y`

implies`y ~ x`

symm : {x y : α} → r x y → r y xAn equivalence relation is transitive:

`x ~ y`

and`y ~ z`

implies`x ~ z`

trans : {x y z : α} → r x y → r y z → r x z

An equivalence relation `~ : α → α → Prop`

is a relation that is:

- reflexive:
`x ~ x`

- symmetric:
`x ~ y`

implies`y ~ x`

- transitive:
`x ~ y`

and`y ~ z`

implies`x ~ z`

Equality is an equivalence relation, and equivalence relations share many of
the properties of equality. In particular, `Quot α r`

is most well behaved
when `r`

is an equivalence relation, and in this case we use `Quotient`

instead.

## Instances For

The empty relation is the relation on `α`

which is always `False`

.

## Equations

- emptyRelation x x = False

`Subrelation q r`

means that `q ⊆ r`

or `∀ x y, q x y → r x y`

.
It is the analogue of the subset relation on relations.

## Equations

- Subrelation q r = ({x y : α} → q x y → r x y)

- base: ∀ {α : Sort u} {r : α → α → Prop} (a b : α), r a b → TC r a b
If

`r a b`

then`r⁺ a b`

. This is the base case of the transitive closure. - trans: ∀ {α : Sort u} {r : α → α → Prop} (a b c : α), TC r a b → TC r b c → TC r a c
The transitive closure is transitive.

The transitive closure `r⁺`

of a relation `r`

is the smallest relation which is
transitive and contains `r`

. `r⁺ a z`

if and only if there exists a sequence
`a r b r ... r z`

of length at least 1 connecting `a`

to `z`

.

## Instances For

# Subtype #

## Equations

- Subtype.instInhabitedSubtype h = { default := { val := a, property := h } }

## Equations

- One or more equations did not get rendered due to their size.

# Sum #

## Equations

- One or more equations did not get rendered due to their size.

# Product #

## Equations

- One or more equations did not get rendered due to their size.

## Equations

- Prod.lexLtDec x x = inferInstanceAs (Decidable (x.fst < x.fst ∨ x.fst = x.fst ∧ x.snd < x.snd))

# Dependent products #

# Universe polymorphic unit #

## Equations

## Equations

- instInhabitedPUnit = { default := PUnit.unit }

## Equations

- instDecidableEqPUnit a b = isTrue (_ : a = b)

# Setoid #

`x ≈ y`

is the distinguished equivalence relation of a setoid.r : α → α → PropThe relation

`x ≈ y`

is an equivalence relation.iseqv : Equivalence r

A setoid is a type with a distinguished equivalence relation, denoted `≈`

.
This is mainly used as input to the `Quotient`

type constructor.

## Instances

# Propositional extensionality #

The axiom of **propositional extensionality**. It asserts that if propositions
`a`

and `b`

are logically equivalent (i.e. we can prove `a`

from `b`

and vice versa),
then `a`

and `b`

are *equal*, meaning that we can replace `a`

with `b`

in all
contexts.

For simple expressions like `a ∧ c ∨ d → e`

we can prove that because all the logical
connectives respect logical equivalence, we can replace `a`

with `b`

in this expression
without using `propext`

. However, for higher order expressions like `P a`

where
`P : Prop → Prop`

is unknown, or indeed for `a = b`

itself, we cannot replace `a`

with `b`

without an axiom which says exactly this.

This is a relatively uncontroversial axiom, which is intuitionistically valid.
It does however block computation when using `#reduce`

to reduce proofs directly
(which is not recommended), meaning that canonicity,
the property that all closed terms of type `Nat`

normalize to numerals,
fails to hold when this (or any) axiom is used:

```
set_option pp.proofs true
def foo : Nat := by
have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩
have := propext this ▸ (2 : Nat)
exact this
#reduce foo
-- propext { mp := fun x x => True.intro, mpr := fun x => True.intro } ▸ 2
#eval foo -- 2
```

`#eval`

can evaluate it to a numeral because the compiler erases casts and
does not evaluate proofs, so `propext`

, whose return type is a proposition,
can never block it.

# Quotients #

The **quotient axiom**, or at least the nontrivial part of the quotient
axiomatization. Quotient types are introduced by the `init_quot`

command
in `Init.Prelude`

which introduces the axioms:

```
opaque Quot {α : Sort u} (r : α → α → Prop) : Sort u
opaque Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
opaque Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
(∀ a b : α, r a b → f a = f b) → Quot r → β
opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
(∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q
```

All of these axioms are true if we assume `Quot α r = α`

and `Quot.mk`

and
`Quot.lift`

are identity functions, so they do not add much. However this axiom
cannot be explained in that way (it is false for that interpretation), so the
real power of quotient types come from this axiom.

It says that the quotient by `r`

maps elements which are related by `r`

to equal
values in the quotient. Together with `Quot.lift`

which says that functions
which respect `r`

can be lifted to functions on the quotient, we can deduce that
`Quot α r`

exactly consists of the equivalence classes with respect to `r`

.

It is important to note that `r`

need not be an equivalence relation in this axiom.
When `r`

is not an equivalence relation, we are actually taking a quotient with
respect to the equivalence relation generated by `r`

.

`Quot.liftOn q f h`

is the same as `Quot.lift f h q`

. It just reorders
the argument `q : Quot r`

to be first.

## Equations

- Quot.liftOn q f c = Quot.lift f c q

Dependent recursion principle for `Quot`

. This constructor can be tricky to use,
so you should consider the simpler versions if they apply:

`Quot.lift`

, for nondependent functions`Quot.ind`

, for theorems / proofs of propositions about quotients`Quot.recOnSubsingleton`

, when the target type is a`Subsingleton`

`Quot.hrecOn`

, which uses`HEq (f a) (f b)`

instead of a`sound p ▸ f a = f b`

assummption

## Equations

- One or more equations did not get rendered due to their size.

Dependent recursion principle for `Quot`

. This constructor can be tricky to use,
so you should consider the simpler versions if they apply:

`Quot.lift`

, for nondependent functions`Quot.ind`

, for theorems / proofs of propositions about quotients`Quot.recOnSubsingleton`

, when the target type is a`Subsingleton`

`Quot.hrecOn`

, which uses`HEq (f a) (f b)`

instead of a`sound p ▸ f a = f b`

assummption

## Equations

- Quot.recOn q f h = Quot.rec f h q

Dependent induction principle for a quotient, when the target type is a `Subsingleton`

.
In this case the quotient's side condition is trivial so any function can be lifted.

Heterogeneous dependent recursion principle for a quotient.
This may be easier to work with since it uses `HEq`

instead of
an `Eq.ndrec`

in the hypothesis.

## Equations

- Quot.hrecOn q f c = Quot.recOn q f (_ : ∀ (a b : α) (p : r a b), (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b)

The canonical quotient map into a `Quotient`

.
(This synthesizes the setoid by typeclass inference.)

## Equations

- Quotient.mk' a = Quotient.mk s a

The analogue of `Quot.sound`

: If `a`

and `b`

are related by the equivalence relation,
then they have equal equivalence classes.

## Equations

The analogue of `Quot.lift`

: if `f : α → β`

respects the equivalence relation `≈`

,
then it lifts to a function on `Quotient s`

such that `lift f h (mk a) = f a`

.

## Equations

- Quotient.lift f = Quot.lift f

The analogue of `Quot.liftOn`

: if `f : α → β`

respects the equivalence relation `≈`

,
then it lifts to a function on `Quotient s`

such that `lift (mk a) f h = f a`

.

## Equations

- Quotient.liftOn q f c = Quot.liftOn q f c

The analogue of `Quot.rec`

for `Quotient`

. See `Quot.rec`

.

## Equations

- Quotient.rec f h q = Quot.rec f h q

The analogue of `Quot.recOn`

for `Quotient`

. See `Quot.recOn`

.

## Equations

- Quotient.recOn q f h = Quot.recOn q f h

The analogue of `Quot.recOnSubsingleton`

for `Quotient`

. See `Quot.recOnSubsingleton`

.

## Equations

The analogue of `Quot.hrecOn`

for `Quotient`

. See `Quot.hrecOn`

.

## Equations

- Quotient.hrecOn q f c = Quot.hrecOn q f c

Lift a binary function to a quotient on both arguments.

## Equations

- One or more equations did not get rendered due to their size.

Lift a binary function to a quotient on both arguments.

## Equations

- Quotient.liftOn₂ q₁ q₂ f c = Quotient.lift₂ f c q₁ q₂

Lift a binary function to a quotient on both arguments.

## Equations

- Quotient.recOnSubsingleton₂ q₁ q₂ g = Quot.recOnSubsingleton q₁ fun a => Quot.recOnSubsingleton q₂ fun a_1 => g a a_1

## Equations

- One or more equations did not get rendered due to their size.

# Function extensionality #

**Function extensionality** is the statement that if two functions take equal values
every point, then the functions themselves are equal: `(∀ x, f x = g x) → f = g`

.
It is called "extensionality" because it talks about how to prove two objects are equal
based on the properties of the object (compare with set extensionality,
which is `(∀ x, x ∈ s ↔ x ∈ t) → s = t`

).

This is often an axiom in dependent type theory systems, because it cannot be proved
from the core logic alone. However in lean's type theory this follows from the existence
of quotient types (note the `Quot.sound`

in the proof, as well as the `show`

line
which makes use of the definitional equality `Quot.lift f h (Quot.mk x) = f x`

).

# Squash #

`Squash α`

is the quotient of `α`

by the always true relation.
It is empty if `α`

is empty, otherwise it is a singleton.
(Thus it is unconditionally a `Subsingleton`

.)
It is the "universal `Subsingleton`

" mapped from `α`

.

It is similar to `Nonempty α`

, which has the same properties, but unlike
`Nonempty`

this is a `Type u`

, that is, it is "data", and the compiler
represents an element of `Squash α`

the same as `α`

itself
(as compared to `Nonempty α`

, whose elements are represented by a dummy value).

`Squash.lift`

will extract a value in any subsingleton `β`

from a function on `α`

,
while `Nonempty.rec`

can only do the same when `β`

is a proposition.

# Relations #

# Kernel reduction hints #

When the kernel tries to reduce a term `Lean.reduceBool c`

, it will invoke the Lean interpreter to evaluate `c`

.
The kernel will not use the interpreter if `c`

is not a constant.
This feature is useful for performing proofs by reflection.

Remark: the Lean frontend allows terms of the from `Lean.reduceBool t`

where `t`

is a term not containing
free variables. The frontend automatically declares a fresh auxiliary constant `c`

and replaces the term with
`Lean.reduceBool c`

. The main motivation is that the code for `t`

will be pre-compiled.

Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base. This is extra 30k lines of code. More importantly, you will probably not be able to check your development using external type checkers (e.g., Trepplein) that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your development using external checkers.

Recall that the compiler trusts the correctness of all `[implemented_by ...]`

and `[extern ...]`

annotations.
If an extern function is executed, then the trusted code base will also include the implementation of the associated
foreign function.

Similar to `Lean.reduceBool`

for closed `Nat`

terms.

Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α) : α := a`

.
The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
We believe `Lean.reduceBool`

enables most interesting applications (e.g., proof by reflection).

The axiom `ofReduceBool`

is used to perform proofs by reflection. See `reduceBool`

.

This axiom is usually not used directly, because it has some syntactic restrictions.
Instead, the `native_decide`

tactic can be used to prove any proposition whose
decidability instance can be evaluated to `true`

using the lean compiler / interpreter.

Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base. This is extra 30k lines of code. More importantly, you will probably not be able to check your development using external type checkers (e.g., Trepplein) that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your development using external checkers.

The axiom `ofReduceNat`

is used to perform proofs by reflection. See `reduceBool`

.

Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base. This is extra 30k lines of code. More importantly, you will probably not be able to check your development using external type checkers (e.g., Trepplein) that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your development using external checkers.

An associative operation satisfies

`(a ∘ b) ∘ c = a ∘ (b ∘ c)`

.assoc : ∀ (a b c : α), op (op a b) c = op a (op b c)

`IsAssociative op`

says that `op`

is an associative operation,
i.e. `(a ∘ b) ∘ c = a ∘ (b ∘ c)`

. It is used by the `ac_rfl`

tactic.

## Instances

A commutative operation satisfies

`a ∘ b = b ∘ a`

.comm : ∀ (a b : α), op a b = op b a

`IsCommutative op`

says that `op`

is a commutative operation,
i.e. `a ∘ b = b ∘ a`

. It is used by the `ac_rfl`

tactic.

## Instances

An idempotent operation satisfies

`a ∘ a = a`

.idempotent : ∀ (x : α), op x x = x

`IsIdempotent op`

says that `op`

is an idempotent operation,
i.e. `a ∘ a = a`

. It is used by the `ac_rfl`

tactic
(which also simplifies up to idempotence when available).

## Instances

A neutral element can be cancelled on the left:

`e ∘ a = a`

.left_neutral : ∀ (a : α), op neutral a = aA neutral element can be cancelled on the right:

`a ∘ e = a`

.right_neutral : ∀ (a : α), op a neutral = a

`IsNeutral op e`

says that `e`

is a neutral operation for `op`

,
i.e. `a ∘ e = a = e ∘ a`

. It is used by the `ac_rfl`

tactic
(which also simplifies neutral elements when available).