关于：redundantMatchAlt
当永远无法达到模式匹配中的替代值时，就会发生此错误：任何可能会出现的值 匹配提供的模式也将匹配一些前面的替代方案。请参阅 模式匹配 手册部分了解更多详细信息 关于模式匹配。
此错误可能出现在任何模式匹配表达式中，包括
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 表达式、方程函数定义、if let
绑定，以及带有后备子句的一元 Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let 绑定。
在多臂模式匹配中，如果不太具体的模式出现在 它所包含的更具体的一项。请记住，表达式与来自的模式相匹配 从上到下，因此特定模式应先于通用模式。
在 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.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let 绑定中
子句中，仅指定了一种模式，此错误表明指定的模式
总是会匹配的。在这种情况下，有问题的绑定可以替换为标准
模式匹配Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let。
导致此错误的一个常见原因是用于匹配构造函数的模式是
相反，解释为变量绑定。例如，如果构造函数
名称（例如，cons）在该类型的命名空间之外写入时没有前缀（List）。
默认情况下启用的构造函数名称作为变量 linter 将在任何变量上显示警告
类似于构造函数名称的模式。
此错误几乎总是表明出现该错误的代码存在问题。不过，如果需要的话，
set_option match.ignoreUnusedAlts true 将禁用对此错误的检查并允许模式
与通过丢弃未使用的臂来编译的冗余替代品进行匹配。
示例
Incorrect Ordering of Pattern Matches
由于任何匹配 (_ :: x :: _) :: xss 的表达式也将匹配 _ :: xss，所以最后一个
在损坏的实现中永远无法实现替代方案。我们通过移动更多来解决这个问题
在更一般的选择之前有特定的选择。