7. 定义🔗

Lean 中以下命令属于“定义式”：

• def

• abbrev

• example

• theorem

• opaque

这些命令都会促使 Lean 的 精译器基于其 签名对一个项进行精译。 除 Lean.Parser.Command.exampleexample（其结果会被丢弃）之外，精译得到的 Lean 核心语言表达式都会保存到环境中以供后续使用。 Lean.Parser.Command.declaration : commandinstance 命令见 实例声明一节。

1. 7.1. 修饰符
2. 7.2. 头部与签名
3. 7.3. 定义
4. 7.4. 定理
5. 7.5. 示例声明
6. 7.6. 递归定义