Functions, inductive types, structures — Interactive Theorem Proving using Lean, Lecture 3

Interactive Theorem Proving using Lean — Lecture 3 University of Freiburg, winter term 2026/27 How types are built in Lean. The commands #check, #eval and #print, and the universe hierarchy. Function types as Π-types: defining functions, anonymous functions, functions whose result type depends on the argument, polymorphic functions and implicit arguments. Inductive types with their constructors, Option and disjunction among them. Structures as inductive types with a single constructor, with fields that may be proofs, and Fin n and ∧ as examples from Lean's Prelude. Course notes: https://pfaffelh.github.io/leancourse/ Slides: https://pfaffelh.github.io/leancourse/slid... Exercises: https://github.com/pfaffelh/leancourse_exe... Proof game: https://pfaffelh.github.io/ipm Lean: https://lean-lang.org/ Mathlib: https://leanprover-community.github.io/ CHAPTERS 00:00 Functions, inductive types, structures 00:22 Every term has a type 02:57 Four steps for every type 04:17 Commands for terms 04:43 In Lean: #check, #eval, #print 05:55 #print shows the proof term 06:07 In Lean: #print of a theorem 07:14 The universe hierarchy 10:02 Function types and Π-types 10:22 In Lean: Π-types and ∀ 14:23 Defining functions 15:17 In Lean: partial application 16:19 Anonymous functions 17:30 In Lean: anonymous functions 18:25 Dependent functions 19:09 In Lean: sevenMod : (n : ℕ) → ZMod n 20:28 Polymorphic functions 20:54 In Lean: implicit arguments, @ and Sort 24:49 Proofs as arguments 25:46 Inductive types 26:35 More inductive types 28:17 ℕ∞ is Option ℕ 29:18 Disjunction is an inductive type 29:49 Structures 31:12 In Lean: a structure Point 32:53 Building values 33:29 Defaults and extensions 34:28 Data with a property 35:30 In Lean: IntAddMap 36:15 Fin n and ∧ are structures 37:16 Structures and inductive types 40:25 Summary