Learning objectives. By the end of this chapter, read a Lean term’s
type with #check, distinguish #check from #eval, write basic defs
with implicit arguments, understand what makes a type dependent (via
Fin/Vec), and state precisely how Π-types, Σ-types, and Prop
irrelevance fit into Lean’s underlying calculus.
Sections
- Everything has a type
def, let, implicit arguments- Dependent types, with examples
- Terminology encountered before it is fully explained
- Π/Σ-types and the calculus of constructions
- Exercises