7. Definitions🔗

The following commands in Lean are definition-like:

• def

• abbrev

• example

• theorem

• opaque

All of these commands cause Lean to elaborate a term based on a signature. With the exception of Lean.Parser.Command.exampleexample, which discards the result, the resulting expression in Lean's core language is saved for future use in the environment. The Lean.Parser.Command.declaration : commandinstance command is described in the section on instance declarations.

1. 7.1. Modifiers
2. 7.2. Headers and Signatures
3. 7.3. Definitions
4. 7.4. Theorems
5. 7.5. Example Declarations
6. 7.6. Recursive Definitions