Foundations
Lean is highly expressive despite having only a few kinds of expression.[…]For the moment, we omit expressions related to quotient types, and effectively consider a sublanguage. Every type is either a universe in the universe hierarchy, a function type, or arises from the type constructor of an inductive type. The remaining expressions can be organized along two axes:
| introduction | elimination | |
|---|---|---|
| function | \lambda-abstraction | evaluation |
| inductive type | constructor | recursor |
We present the formation, introduction, elimination, and reduction rules for functions and inductive types. We also discuss when two functions, and two expressions of an inductive type, are equal.