7. 定义🔗

Lean 中以下命令属于“定义式（definition-like）”：

• def

• abbrev

• example

• theorem

• opaque

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

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