10. Terms🔗

Terms are the principal means of writing mathematics and programs in Lean. The elaborator translates them to Lean's minimal core language, which is then checked by the kernel and compiled for execution. The syntax of terms is arbitrarily extensible; this chapter documents the term syntax that Lean provides out-of-the-box.

1. 10.1. Identifiers
2. 10.2. Function Types
3. 10.3. Functions
4. 10.4. Function Application
5. 10.5. Literals
6. 10.6. Structures and Constructors
7. 10.7. Conditionals
8. 10.8. Pattern Matching
9. 10.9. Holes
10. 10.10. Type Ascription
11. 10.11. Quotation and Antiquotation
12. 10.12. do-Notation
13. 10.13. Proofs