7. Definitions🔗

The following commands in Lean are definition-like: Render commands as their name (a la tactic index)

• 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