7.4. 定理🔗

由于命题是其占据元可作为证明的类型，定理与“定义”在技术上非常相似。然而，由于它们的使用场景不同，许多细节上有所差异：

定理陈述必须是一个命题；而定义的类型可以属于任意宇宙。
定理的头部（即定理陈述）会在定理主体之前被完全精译。只有当区段变量（或依赖于它们的变量）出现在头部时，它们才会成为定理的参数。这可以避免更改证明时无意间改变定理陈述本身。
定理默认是不可约的。由于对同一命题的所有证明在定义相等下是相等的，几乎没有理由去展开一个定理。

定理也可以是递归的，但需满足与递归函数定义相同的条件。不过，更常见的做法是使用 induction 或 fun_induction 等策略来完成证明。

语法定理

定理的语法与定义类似，但签名中的余域（即定理陈述）是强制的。

command ::= ...
    | `declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers
      theorem `declId` 匹配 `foo` 或 `foo.{u,v}`：一个标识符，后面可以跟一个宇宙名称列表。declId `declSig` 匹配类型必需的声明签名：先是一列绑定器，随后是 `: type`。declSig := term终止提示依次为 `termination_by` 和 `decreasing_by`。

command ::= ...
    | `declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers
      theorem `declId` 匹配 `foo` 或 `foo.{u,v}`：一个标识符，后面可以跟一个宇宙名称列表。declId `declSig` 匹配类型必需的声明签名：先是一列绑定器，随后是 `: type`。declSig
        (| term => term)*终止提示依次为 `termination_by` 和 `decreasing_by`。

command ::= ...
    | `declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers
      theorem `declId` 匹配 `foo` 或 `foo.{u,v}`：一个标识符，后面可以跟一个宇宙名称列表。declId `declSig` 匹配类型必需的声明签名：先是一列绑定器，随后是 `: type`。declSig where
        structInstField*

在模块中，定理的证明默认不会对外公开。