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. 递归定义