定义或声明的 头部（若有）由待声明/定义的常量以及其签名组成。 常量的 签名 指定了它可以如何被使用。 签名中包含的不仅仅是类型本身的信息，还包括例如 宇宙层级参数、可选参数的默认值等。 在 Lean 中，不同类型的声明均使用一致的格式来书写签名。
大多数头部以一个 声明名称 开始，随后是其真正的签名：参数列表以及结果类型。 一个声明名称可以可选地包含宇宙层级参数。
不带宇宙参数的声明名称仅由一个标识符组成：
declId ::=
`declId` 匹配 `foo` 或 `foo.{u,v}`：一个标识符，后面可以跟一个宇宙名称列表。带宇宙参数的声明名称由一个标识符，后接一个点与一组花括号中的一个或多个宇宙参数名构成：
declId ::= ...
| `declId` 匹配 `foo` 或 `foo.{u,v}`：一个标识符，后面可以跟一个宇宙名称列表。这些宇宙参数名是绑定出现。
示例不包含声明名称；而实例声明的名字是可选的。
一个签名由零个或多个参数构成，后跟一个冒号与一个类型：
declSig ::=(ident |`declSig` 匹配类型必需的声明签名：先是一列绑定器，随后是 `: 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` 匹配类型可选的声明签名：先是一列绑定器，随后可以有 `: 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).
参数可以有三种形式：
标识符：为参数命名，但不提供类型。这类参数的类型必须在精译阶段推断出来。
下划线（_）：表示该参数在局部作用域中不能通过名字访问。这类参数的类型同样需要在精译阶段推断。
带括号参数：可以为一个或多个参数指定所有方面的信息，包括名称、类型、默认值，以及其是显式、隐式、严格隐式或实例隐式。
除标识符与下划线外的其它参数形式统称为 带括号参数，因为它们的语法形式都使用了某种括号（圆括号、花括号或方括号）。
所有带括号参数都会显式给出参数类型，并且多数情况下也会包含参数名。
对于“实例隐式”参数，名字是可选的。
用下划线（_）替代参数名表示匿名参数。
使用圆括号括起的参数表示显式参数。 如果提供了多个标识符或下划线，则它们都会成为具有相同类型的多个参数：
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
对于未显式标注类型的参数，其宇宙参数会被自动插入。
即便禁用了 autoImplicit，类型参数所处的宇宙也可被推断，并插入相应的宇宙参数：
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
由于 区段变量引入的参数会先被插入，自动隐式参数的插入发生在其之后。 与节变量对应的参数即便并未直接对应于签名中书写的某个名字，仍会与其对应的节变量同名；而禁用自动隐式参数对这些对应于节变量的参数不起作用。 不过，当启用自动隐式参数时，包含其他未绑定变量的节变量声明还会获得遵循与隐式参数相同规则的附加节变量。
自动隐式参数的插入由两个选项控制。
默认情况下，该插入处于“宽松”模式，这意味着任何未绑定的标识符都可能成为自动插入的候选。
将 relaxedAutoImplicit 设为 false 会禁用宽松模式，此时仅由“单个字母后跟零个或多个数字”构成的标识符才会被考虑用于自动插入。
autoImplicit
拼写错误的标识符或缺失的导入，可能会变成意外的隐式参数，如下例所示：
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