term ::= ... |match ((generalizing := (trueVal | falseVal)))? ((motive := term))?Pattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not.matchDiscr,* with (| (term,*)|* => term)*`matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as `match h1 : e1, e2, h3 : e3 with ...`.
13.8. 模式匹配
模式匹配是一种使用 模式 语法来识别和解构值的方法，模式是术语的子集。
识别和解构值的模式类似于用于构造值的语法。
一个或多个 匹配判别式同时与一系列 匹配替代项进行比较。
判别式可以被命名。
每个替代项都包含一个或多个以逗号分隔的模式序列；所有模式序列必须包含与判别式相同数量的模式。
当模式序列与所有判别式匹配时，在用每个 模式变量 的值以及每个命名判别式的等式假设扩展的环境中评估相应 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
=> 后面的项。
该术语称为匹配替代项的 右侧。
syntaxPattern Matching
syntaxMatch Discriminants
matchDiscr ::=
`matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as
`match h1 : e1, e2, h3 : e3 with ...`. matchDiscr ::= ...
| `matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as
`match h1 : e1, e2, h3 : e3 with ...`.
模式匹配表达式也可以使用 quasiquotations 作为模式，匹配相应的 Lean.Syntax 值并将 antiquotations 的内容视为普通模式。
引用模式的编译方式与其他模式不同，因此如果 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match 中的一种模式是语法，那么所有模式都必须是语法。
报价模式在 报价部分中描述。
模式是术语的子集。 它们由以下部分组成：
- 包罗万象的模式
空洞语法
_是一种匹配任何值且不绑定任何模式变量的模式。 包罗万象的模式并不完全等同于未使用的模式变量。 它们可以用在模式输入需要更具体的 无法访问的模式的位置，而变量不能在这些位置使用。- 标识符
如果标识符未绑定在当前范围内且未应用于参数，则它表示模式变量。 Pattern 变量 匹配任何值，并且如此匹配的值将绑定到计算 右侧 的本地环境中的模式变量。 如果标识符已绑定，则如果它绑定到 归纳类型 的 构造函数，或者其定义具有
match_pattern属性，则它是一个模式。- 应用领域
如果所应用的函数是绑定到构造函数的标识符或具有
match_pattern属性并且所有参数也是模式，则函数应用程序是模式。 如果标识符是构造函数，则当参数模式与构造函数的参数匹配时，模式将匹配使用该构造函数构建的值。 如果它是具有match_pattern属性的函数，则展开函数应用程序，并将结果项的 正规形式 用作模式。 默认参数照常插入，并且它们的正常形式用作模式。 然而，省略号 会导致所有其他参数被视为通用模式，即使是那些具有关联默认值或策略的参数。- 文字
字符文字 和 字符串文字 是与相应字符或字符串匹配的模式。 原始字符串文字 允许作为模式，但 插值字符串 不允许作为模式。 模式中的 自然数文字 通过合成相应的
OfNat实例并将结果项减少为 正常形式（它必须是模式）来解释。 同样，科学文字 通过相应的OfScientific实例进行解释。 虽然Float有这样的实例，但Float不能用作模式，因为该实例依赖于无法简化为有效模式的不透明函数。- 结构实例
结构实例可以用作模式。 它们被解释为相应的结构构造函数。
- 引用的名字
Quoted names, such as
`xand``none, match the correspondingLean.Namevalue.- 宏
模式中的宏被扩展。 如果产生的扩展是模式，那么它们就是模式。
- 无法访问的模式
不可访问的模式 是通过稍后键入约束而强制具有特定值的模式。 任何术语都可以用作不可访问的术语。 无法访问的术语用括号括起来，前面带有句点 (
.)。
syntaxInaccessible Patterns
term ::= ...
| `.(e)` marks an "inaccessible pattern", which does not influence evaluation of the pattern match, but may be necessary for type-checking.
In contrast to regular patterns, `e` may be an arbitrary term of the appropriate type.
Inaccessible Patterns
数字的奇偶性是它是偶数还是奇数：
inductive Parity : Nat → Type where
| even (h : Nat) : Parity (h + h)
| odd (h : Nat) : Parity ((h + h) + 1)
def Nat.parity (n : Nat) : Parity n :=
match n with
| 0 => .even 0
| n' + 1 =>
match n'.parity with
| .even h => .odd h
| .odd h =>
have eq : (h + 1) + (h + 1) = (h + h + 1 + 1) :=
n:Nath:Nat⊢ h + 1 + (h + 1) = h + h + 1 + 1 All goals completed! 🐙
eq ▸ .even (h + 1)
由于 Parity 类型的值包含数字的一半（向下舍入）作为其偶数或奇数表示的一部分，因此可以通过查找奇偶校验然后提取数字来实现除以二（以非常规方式）。
def half (n : Nat) : Nat :=
match n, n.parity with
| .(h + h), .even h => h
| .(h + h + 1), .odd h => h
由于 Parity.even 和 Parity.odd 的索引结构强制数字具有某种形式，否则该形式不是有效模式，因此与其匹配的模式必须对被除数使用不可访问的模式。
还可以对模式进行命名。
命名模式将名称与模式关联起来；在后续模式中以及匹配替代项的右侧，名称指的是与给定模式匹配的值的部分。
命名模式在名称和模式之间写入 @。
就像判别式一样，命名模式也可以提供用于相等假设的名称。
syntaxNamed Patterns
term ::= ...
| `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
If present, the identifier `h` is bound to a proof of `x = e`. term ::= ...
| `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
If present, the identifier `h` is bound to a proof of `x = e`. 13.8.1. 类型
每个判别式都必须有良好的类型。 由于模式是术语的子集，因此也可以检查它们的类型。 与给定判别式匹配的每个模式必须与相应的判别式具有相同的类型。
每个匹配替代项的 右侧 应具有与整体 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match 术语相同的类型。
为了支持 依值类型，将判别式与模式匹配可以细化模式范围内预期的类型。
在同一匹配替代项和右侧类型中的两个后续模式中，判别式的出现将被替换为它所匹配的模式。
Type Refinement
这个 索引族 描述了大部分平衡的树，深度编码在类型中。
inductive BalancedTree (α : Type u) : Nat → Type u where
| empty : BalancedTree α 0
| branch
(left : BalancedTree α n)
(val : α)
(right : BalancedTree α n) :
BalancedTree α (n + 1)
| lbranch
(left : BalancedTree α (n + 1))
(val : α)
(right : BalancedTree α n) :
BalancedTree α (n + 2)
| rbranch
(left : BalancedTree α n)
(val : α)
(right : BalancedTree α (n + 1)) :
BalancedTree α (n + 2)
要开始实现函数来构造具有某些初始元素和给定深度的完美平衡树，可以使用 hole 进行定义。
def BalancedTree.filledWith
(x : α) (depth : Nat) :
BalancedTree α depth :=
_
错误消息表明树应该具有指示的深度。
匹配预期深度并插入孔会导致每个孔出现错误消息。
这些消息表明预期类型已被细化，depth 被匹配的值替换。
def BalancedTree.filledWith
(x : α) (depth : Nat) :
BalancedTree α depth :=
match depth with
| 0 => _
| n + 1 => _
第一个洞产生以下消息：
第二个洞产生以下消息：
树的深度和树本身的匹配会根据深度的模式对树的类型进行细化。
这意味着某些组合的类型不正确，例如 0 和 branch，因为细化第二个判别式的类型会生成与构造函数的类型不匹配的 BalancedTree α 0。
def BalancedTree.isPerfectlyBalanced
(n : Nat) (t : BalancedTree α n) : Bool :=
match n, t with
| 0, .empty => true
| 0, .branch left val right =>
isPerfectlyBalanced left &&
isPerfectlyBalanced right
| _, _ => false
13.8.1.1. 模式相等性证明
当命名判别式时，Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match 会生成模式和判别式相等的证明，并将其绑定到 右侧 中提供的名称。
这对于弥合索引系列上的依赖模式匹配与需要显式命题参数的 API 之间的差距非常有用，并且可以帮助利用假设的策略取得成功。
Pattern Equality Proofs
函数 last? 使用标准库函数 List.getLast，它要么引发异常，要么返回其参数的最后一个元素。
此函数需要证明所讨论的列表非空。
将比赛命名为 xs 可确保范围内存在一个假设，即 xs 等于 _ :: _，simp_all 使用该假设来实现目标。
def last? (xs : List α) : Except String α :=
match h : xs with
| [] =>
.error "Can't take first element of empty list"
| _ :: _ =>
.ok <| xs.getLast (show xs ≠ [] All goals completed! 🐙 α:Type ?u.3xs:List αhead✝:αtail✝:List αh:xs = head✝ :: tail✝h':xs = []⊢ False; All goals completed! 🐙)
没有名字，simp_all就无法找到矛盾。
def last?' (xs : List α) : Except String α :=
match xs with
| [] =>
.error "Can't take first element of empty list"
| _ :: _ =>
.ok <| xs.getLast (show xs ≠ [] α:Type ?u.3xs:List αhead✝:αtail✝:List αh':xs = []⊢ False α:Type ?u.3xs:List αhead✝:αtail✝:List αh':xs = []⊢ False; α:Type ?u.3xs:List αhead✝:αtail✝:List αh':xs = []⊢ False)
13.8.1.2. 明确的动机
模式匹配不是 Lean 的内置原语。
相反，它通过 辅助匹配函数 转换为 递归器 的应用程序。
两者都需要 motive 来解释判别式和结果类型之间的关系。
一般来说，Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match精化器能够合成适当的动机，并且模式匹配期间发生的类型细化是所选动机的结果。
在某些特殊情况下，可能需要不同的动机，并且可以使用 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match 的 (motive := …) 语法显式提供。
这个动机应该是一个函数类型，它期望至少与判别式一样多的参数。
将具有此类型的函数按顺序应用于判别式所产生的类型是整个 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match 项的类型，而将具有此类型的函数应用于每个替代中的所有模式所产生的类型是该替代的 右侧 的类型。
13.8.1.3. 判别式细化
当匹配索引族时，索引也必须是判别式。 否则，该模式的类型不会很好：如果索引只是一个变量但构造函数的类型需要更具体的值，则这是一个类型错误。 然而，一个名为 判别细化 的过程会自动添加索引作为附加判别式。
13.8.1.4. 概括
模式匹配精化器通过查找预期类型中判别式的出现来自动确定动机，将它们概括为后续判别式的类型，以便可以替换适当的模式。
此外，默认情况下，上下文中变量类型中判别式的出现将被概括和替换。
可以通过将 (generalizing := false) 标志传递给 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match 来关闭后一种行为。
Matching, With and Without Generalization
在 boolCases 的定义中，假设 b 被概括为 h 的类型，然后替换为实际模式。
这意味着 ifTrue 和 ifFalse 在各自的情况下具有类型 true = true → α 和 false = false → α，但 h 的类型提到了原始判别式。
def boolCases (b : Bool)
(ifTrue : b = true → α)
(ifFalse : b = false → α) :
α :=
match h : b with
| true => ifTrue h
| false => ifFalse h
第一种情况的错误是两种情况的典型错误：
关闭泛化可以使类型检查成功，因为 b 仍保留在 ifTrue 和 ifFalse 的类型中。
def boolCases (b : Bool)
(ifTrue : b = true → α)
(ifFalse : b = false → α) :
α :=
match (generalizing := false) h : b with
| true => ifTrue h
| false => ifFalse h
在通用版本中，rfl 可以用作证明参数作为替代方案。
13.8.2. 自定义模式功能
在模式中，使用 match_pattern 属性定义的常量将展开并规范化，而不是拒绝。
这允许对许多模式使用更方便的语法。
在标准库中，Nat.add、HAdd.hAdd、Add.add 和 Neg.neg 都具有此属性，该属性允许像 n + 1 这样的模式而不是 Nat.succ n。
类似地，Unit和Unit.unit是将PUnit和PUnit.unit各自的宇宙参数设置为0的定义； Unit.unit 上的 match_pattern 属性允许其在模式中使用，并扩展为 PUnit.unit.{0}。
attributeAttribute for Match Patterns
match_pattern 属性指示应在模式中展开而不是拒绝定义。
attr ::= ... | match_pattern
Match Patterns Follow Reduction
以下函数无法编译：
def nonzero (n : Nat) : Bool :=
match n with
| 0 => false
| 1 + k => true
模式 1 + _ 上的错误消息是：
这是因为 Nat.add 是通过其第二个参数的递归定义的，相当于：
def add : Nat → Nat → Nat
| a, Nat.zero => a
| a, Nat.succ b => Nat.succ (Nat.add a b)
ι-reduction 是不可能的，因为匹配的值是变量，而不是构造函数。
1 + k 被卡为 Nat.add 1 k，这不是有效的模式。
对于 k + 1（即 Nat.add k (.succ .zero)），第二个模式匹配，因此它减少为 Nat.succ (Nat.add k .zero)。
现在第二个模式匹配，生成 Nat.succ k，这是一个有效的模式。
13.8.3. 模式匹配功能
syntaxPattern-Matching Functions
可以通过模式匹配指定功能，方法是在 Lean.Parser.Term.fun : termfun 之后编写一系列模式，每个模式前面都有一个竖线 (|)。
term ::= ... | fun (| term,* => term)*
这将脱糖为一个立即对其参数进行模式匹配的函数。
Pattern-Matching Functions
isZero 使用模式匹配函数抽象定义，而 isZero' 使用模式匹配表达式定义：
def isZero : Nat → Bool :=
fun
| 0 => true
| _ => false
def isZero' : Nat → Bool :=
fun n =>
match n with
| 0 => true
| _ => false
因为前者是后者的语法糖，所以它们在定义上是相等的：
example : isZero = isZero' := rfl
脱糖在 Lean.Parser.Command.print : command#print 的输出中可见：
#print isZero
输出
尽管
#print isZero'
输出
13.8.4. 其他模式匹配运营商
除了 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match 和 termIfLet : term`if let pat := d then t else e` is a shorthand syntax for:
```
match d with
| pat => t
| _ => e
```
It matches `d` against the pattern `pat` and the bindings are available in `t`.
If the pattern does not match, it returns `e` instead.
if let 之外，还有一些其他运算符执行模式匹配。
syntaxThe
matches Operator
当对 Lean.«term_Matches_|» : termmatches 的结果进行分支时，通常最好使用 termIfLet : term`if let pat := d then t else e` is a shorthand syntax for:
```
match d with
| pat => t
| _ => e
```
It matches `d` against the pattern `pat` and the bindings are available in `t`.
If the pattern does not match, it returns `e` instead.
if let，它除了检查模式是否匹配之外还可以绑定模式变量。
如果没有可以匹配判别式或判别式序列的构造函数模式，则相关代码将无法访问，因为本地上下文中必定存在错误假设。
Lean.Parser.Term.nomatch : termEmpty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
Lean can show that an empty set of patterns is exhaustive given `e`'s type,
e.g. because it has no constructors.
nomatch 表达式是零个案例的匹配，可以具有任何类型，只要没有可能的案例可以匹配判别式即可。
syntaxCaseless Pattern Matches
term ::= ...
| Empty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
Lean can show that an empty set of patterns is exhaustive given `e`'s type,
e.g. because it has no constructors.
Inconsistent Indices
没有构造函数模式可以匹配此示例中的两个证明：
example (p1 : x = "Hello") (p2 : x = "world") : False :=
nomatch p1, p2
这是因为它们分别将 x 的值细化为不相等的字符串。
因此，Lean.Parser.Term.nomatch : termEmpty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
Lean can show that an empty set of patterns is exhaustive given `e`'s type,
e.g. because it has no constructors.
nomatch 运算符允许示例的主体证明 False（或任何其他命题或类型）。
当预期类型是函数类型时，Lean.Parser.Term.nofun : termnofun 是函数的简写，该函数采用与类型指示的参数一样多的参数，其中主体是应用于所有参数的 Lean.Parser.Term.nomatch : termEmpty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
Lean can show that an empty set of patterns is exhaustive given `e`'s type,
e.g. because it has no constructors.
nomatch。
syntaxCaseless Functions
term ::= ... | nofun
Impossible Functions
可以使用 Lean.Parser.Term.nofun : termnofun，而不是为两个相等证明引入参数，然后在 Lean.Parser.Term.nomatch : termEmpty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
Lean can show that an empty set of patterns is exhaustive given `e`'s type,
e.g. because it has no constructors.
nomatch 中使用两者。
example : x = "Hello" → x = "world" → False := nofun