4. Terms🔗

This chapter will describe Lean's term language, including the following features:

• Name resolution, including variable occurrences, open declarations and terms

• Function application, including implicit, instance, and named arguments

• Leading .-notation and accessor notation

• fun, with and without pattern matching

• Literals (some via cross-references to the appropriate types, e.g. String)

• Conditionals and their relationship to Decidable

• Pattern matching, including match, let, if let, matches, nomatch, nofun

• Do-notation, including let mut, for, while, repeat, break, return

• Holes and named holes

Tracked at issue #66