定义或声明的 header 由声明或定义的常量（如果相关）及其签名组成。 常量的 signature 指定如何使用它。 签名中呈现的信息不仅仅是类型，还包括宇宙层级参数等信息及其可选参数的默认值。 在Lean中，不同类型的声明中的签名都以一致的格式书写。
大多数标头以 declaration name 开头，后面跟着正确的签名：其参数和结果类型。 声明名称是可以选择包含 Universe 参数的名称。
不带 Universe 参数的声明名称由标识符组成：
declId ::=
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names 带有 Universe 参数的声明名称由一个标识符后跟一个句点以及大括号中的一个或多个 Universe 参数名称组成：
declId ::= ...
| `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names 这些 Universe 参数名称是绑定事件。
示例不包括声明名称，并且实例声明的名称是可选的。
名称后面（如果存在）是标头的签名。 签名指定声明的参数和类型。
签名由零个或多个参数组成，后跟冒号和类型。
declSig ::=(ident |`declSig` matches the signature of a declaration with required type: a list of binders and then `: type`hole | bracketedBinder)* : termA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).
签名通常是可选的。 在这些情况下，即使省略类型，也可以提供参数。
optDeclSig ::=(ident |`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`hole | bracketedBinder)* (: term)?A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).
参数可以有三种形式：
标识符，命名参数但不提供类型。 这些参数的类型必须在精化期间推断。
下划线 (_)，表示在本地范围内无法通过名称访问的参数。
这些参数的类型也必须在精化期间推断。
一种带括号的绑定器，它可以指定一个或多个参数的各个方面，包括它们的名称、类型、默认值以及它们是显式的、隐式的、严格隐式的还是实例隐式的。
除标识符或下划线之外的参数统称为 bracketed binders，因为指定它们的每个语法形式都有某种类型的方括号、大括号或圆括号。
所有括号内的绑定程序都指定参数的类型，并且大多数都包含参数名称。
对于实例隐式参数，名称是可选的。
使用下划线 (_) 代替参数名称表示匿名参数。
带括号的参数表示显式参数。 如果提供了多个标识符或下划线，则它们全部成为同一类型的参数。
bracketedBinder ::=((ident |Explicit binder, like `(x y : A)` or `(x y)`. Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.hole) (ident |A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).hole)* : term)A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).
带 := 的括号参数为参数分配默认值。
具有默认值的参数称为 可选参数。
在调用站点，如果未提供参数，则使用提供的术语来填充它。
签名中的先前参数在默认值范围内，并且它们在调用站点的值将替换为默认值项。
如果提供了 策略脚本，则在调用站点执行策略以合成参数值；通过策略填写的参数称为自动参数。
bracketedBinder ::= ... |((ident |Explicit binder, like `(x y : A)` or `(x y)`. Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.hole) (ident |A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).hole)* : term := term)A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).
大括号中的参数表示 隐式 参数。 除非在调用站点通过名称提供，否则这些参数预计将通过调用站点的统一进行合成。 隐式参数在所有调用站点进行综合。
bracketedBinder ::= ... |{(ident |Implicit binder, like `{x y : A}` or `{x y}`. In regular applications, whenever all parameters before it have been specified, then a `_` placeholder is automatically inserted for this parameter. Implicit parameters should be able to be determined from the other arguments and the return type by unification. In `@` explicit mode, implicit binders behave like explicit binders.hole) (ident |A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).hole)* : term}A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).
双花括号中的参数表示 严格隐式 参数。
⦃ … ⦄ 和 {{ … }} 等效。
与隐式参数一样，当未按名称提供这些参数时，预计将通过调用站点的统一来合成这些参数。
仅当还提供了签名中的后续参数时，才会在调用站点合成严格的隐式参数。
bracketedBinder ::= ... |⦃(ident |Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`. In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert a `_` placeholder until at least one subsequent explicit parameter is specified. Do *not* use strict-implicit binders unless there is a subsequent explicit parameter. Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior. Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`, then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter, and `h hs` has type `p y`. In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m` with `?m` a fresh metavariable.hole) (ident |A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).hole)* : term⦄A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).
bracketedBinder ::= ... |{{(ident |Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`. In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert a `_` placeholder until at least one subsequent explicit parameter is specified. Do *not* use strict-implicit binders unless there is a subsequent explicit parameter. Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior. Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`, then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter, and `h hs` has type `p y`. In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m` with `?m` a fresh metavariable.hole) (ident |A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).hole)* : term}}A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).
方括号中的参数表示 实例隐式 参数，这些参数是使用 实例合成 在调用站点合成的。
bracketedBinder ::= ...
| Instance-implicit binder, like `[C]` or `[inst : C]`.
In regular applications without `@` explicit mode, it is automatically inserted
and solved for by typeclass inference for the specified class `C`.
In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
参数始终位于签名类型的范围内，该类型出现在冒号之后。 它们也在声明主体的范围内，而在类型本身中绑定的名称仅在类型的范围内。 因此，参数名称被使用两次：
作为声明函数类型中的名称，绑定为 依赖函数类型 的一部分。
作为声明正文中的名称。
在函数定义中，它们由 Lean.Parser.Term.fun : termfun 绑定。
add 的签名包含一个参数 n。
另外，签名的类型是(k : Nat) → Nat，它是包含k的函数类型。
参数 n 在函数体的范围内，但 k 不在。
def add (n : Nat) : (k : Nat) → Nat
| 0 => n
| k' + 1 => 1 + add n k'
与 add 一样，mustBeEqual 的签名包含一个参数 n。
它在类型中（它出现在命题中）和正文中（它作为消息的一部分出现）都在范围内。
def mustBeEqual (n : Nat) : (k : Nat) → n = k → String :=
fun _ =>
fun
| rfl => s!"Equal - both are {n}!"
默认情况下，签名中出现的其他未绑定名称会在可能的情况下转换为隐式参数 这些参数称为 自动隐式参数。 当它们不处于应用程序的功能位置并且签名中有足够的可用信息来推断它们的类型以及它们的任何排序约束时，这是可能的。 迭代此过程：如果新插入的隐式参数的推断类型具有未唯一确定的依赖项，则这些依赖项将替换为进一步的隐式参数。
与签名中写入的名称不对应的隐式参数被分配的名称类似于证明中 不可访问 假设的名称，无法引用。
它们出现在带有匕首的签名中（'✝'）。
这可以防止 Lean 任意选择的名称通过用作 命名参数 成为 API 的一部分。
在此定义中，α 和 β 没有显式绑定。
由于 autoImplicit 已禁用，因此这是一个错误：
set_option autoImplicit false
def map (f : α → β) : (xs : List α) → List β
| [] => []
| x :: xs => f x :: map f xs
完整的签名允许定义被接受：
set_option autoImplicit false
def map.{u, v} {α : Type u} {β : Type v}
(f : α → β) :
(xs : List α) → List β
| [] => []
| x :: xs => f x :: map f xs
对于没有显式类型注释的参数，将自动插入 Universe 参数。
即使 autoImplicit 被禁用，也可以推断类型参数的 Universe，并插入适当的 Universe 参数：
set_option autoImplicit false
def map {α β} (f : α → β) :
(xs : List α) → List β
| [] => []
| x :: xs => f x :: map f xs
给定一个由 n 界定的数字（由类型 Fin n 表示），AtLeast i 是一个自然数，并且证明它至少与 i 一样大。
structure AtLeast (i : Fin n) where
val : Nat
val_gt_i : val ≥ i.val
可以添加这些数字：
def AtLeast.add (x y : AtLeast i) : AtLeast i :=
AtLeast.mk (x.val + y.val) <| n✝:Nati:Fin n✝x:AtLeast iy:AtLeast i⊢ x.val + y.val ≥ ↑i
n✝:Nati:Fin n✝y:AtLeast ival✝:Natval_gt_i✝:val✝ ≥ ↑i⊢ { val := val✝, val_gt_i := val_gt_i✝ }.val + y.val ≥ ↑i
n✝:Nati:Fin n✝val✝¹:Natval_gt_i✝¹:val✝ ≥ ↑ival✝:Natval_gt_i✝:val✝ ≥ ↑i⊢ { val := val✝¹, val_gt_i := val_gt_i✝¹ }.val + { val := val✝, val_gt_i := val_gt_i✝ }.val ≥ ↑i
n✝:Nati:Fin n✝val✝¹:Natval_gt_i✝¹:val✝ ≥ ↑ival✝:Natval_gt_i✝:val✝ ≥ ↑i⊢ val✝¹ + val✝ ≥ ↑i
All goals completed! 🐙
AtLeast.add的签名需要多轮自动隐式参数插入。
首先插入i；但其类型取决于 Fin n 的上限 n。
在第二轮中，使用机器选择的名称插入 n。
由于 n 的类型是 Nat，它没有依赖性，因此进程终止。
最终签名可以通过 Lean.Parser.Command.check : command#check 看到：
#check AtLeast.add
由于 节变量，在插入参数后会发生自动隐式参数插入。 与节变量相对应的参数具有与相应变量相同的名称，即使它们不与直接写入签名中的名称相对应，并且禁用自动隐式参数不会影响与节变量相对应的参数。 但是，当启用自动隐式参数时，包含其他未绑定变量的节变量声明会接收遵循与隐式参数相同规则的附加节变量。
自动隐式参数插入由两个选项控制。
默认情况下，自动隐式参数插入是relaxed，这意味着任何未绑定的标识符都可以是自动插入的候选者。
将选项 relaxedAutoImplicit 设置为 false 会禁用宽松模式，并导致仅考虑由单个字符后跟零个或多个数字组成的标识符进行自动插入。
relaxedAutoImplicit
Default value: true
When "relaxed" mode is enabled, any atomic nonempty identifier is eligible for auto bound implicit locals (see option autoImplicit).
autoImplicit
Default value: true
Unbound local variables in declaration headers become implicit arguments. In "relaxed" mode (default), any atomic identifier is eligible, otherwise only single character followed by numeric digits are eligible. For example, def f (x : Vector α n) : Vector α n := automatically introduces the implicit variables {α n}.
拼写错误的标识符或丢失的导入最终可能会成为不需要的隐式参数，如下例所示：
inductive Answer where
| yes
| maybe
| no
def select (choices : α × α × α) : Asnwer → α
| .yes => choices.1
| .maybe => choices.2.1
| .no => choices.2.2
生成的错误消息指出参数的类型不是常量，因此点符号不能在模式中使用：
这是因为签名是：
select.{u_1, u_2}
{α : Type u_1}
{Asnwer : Sort u_2}
(choices : α × α × α) :
Asnwer → α禁用宽松的自动隐式参数可以使错误更加清晰，同时仍然允许自动插入类型：
set_option relaxedAutoImplicit false
def select (choices : α × α × α) : Asnwer → α
| .yes => choices.1
| .maybe => choices.2.1
| .no => choices.2.2
纠正错误可以使定义被接受。
set_option relaxedAutoImplicit false
def select (choices : α × α × α) : Answer → α
| .yes => choices.1
| .maybe => choices.2.1
| .no => choices.2.2
关闭自动隐式参数完全会导致定义被拒绝：
set_option autoImplicit false
def select (choices : α × α × α) : Answer → α
| .yes => choices.1
| .maybe => choices.2.1
| .no => choices.2.2