foundational types

Some of Lean's types are not defined in any Lean source files (even the prelude) since they come from its foundational type theory. This page provides basic documentation for these types.

For a more in-depth explanation of Lean's type theory, refer to TPiL.

`Sort u` #

Sort u is the type of types in Lean, and Sort u : Sort (u + 1).

Instances for Sort u

sort.inhabited

`Type u` #

Type u is notation for Sort (u + 1).

Instances for Type u

`Prop` #

Prop is notation for Sort 0.

Instances for Prop

Pi types, `Π a : α, β a` #

The type of dependent functions is known as a pi type. Non-dependent functions and implications are a special case.

Note that these can also be written with the alternative notations:

∀ a : α, β a, conventionally used where β a : Prop.
α → γ, possible only if β a = γ for all a.

Lean also permits ASCII-only spellings of the three variants:

Pi a : A, B a for Π a : α, β a
forall a : A, B a for ∀ a : α, β a
A -> B, for α → β

Note that despite not itself being a function, (→) is available as infix notation for λ α β, α → β.

Instances for Π a : α, β a

Instances for ∀ a : α, β a

Instances for α → β

Instances for P → Q

implies.decidable

foundational types

Sort u #

Type u #

Prop #

Pi types, Π a : α, β a #

`Sort u` #

`Type u` #

`Prop` #

Pi types, `Π a : α, β a` #