关于：propRecLargeElim
当试图将命题的证明消除到更高类型的宇宙中时，会发生此错误。
由于 Lean 的 类型论 不允许从 Prop 进行大量消除，因此无效
对此类值进行模式匹配- 例如，通过使用 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.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 u）。更准确地说，命题递归器的动机必须是一个命题。
（有关例外情况，请参阅手册中有关 Subsingleton Elimination 的部分
遵守此规则。）
请注意，任何将证明消除为证明的表达式都会出现此错误
非命题宇宙，即使该表达式出现在另一个表达式中
命题类型（例如，在证明中的 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 绑定中）。的
下面的“在证明中定义中间数据值”示例演示了这种情况。
此类错误通常可以通过将递归应用程序“向外”移动来解决，以便
它的动机是被证明的命题而不是数据值术语的类型。
示例
Defining an Intermediate Data Value Within a Proof
尽管定义的 Lean.Parser.Command.exampleexample 有一个命题
类型，val 的主体没有；它的类型为 α : Type。因此，证明上的模式匹配
Nonempty α（一个命题）生成 val 需要将该证明消除为
非命题类型，是不允许的。相反，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
表达式必须移至 example 的顶层，其中结果是
示例标题中所述存在性命题的 Prop 值证明。这个
重组也可以使用模式匹配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 来完成
绑定。
Extracting the Witness from an Existential Proof
在这个例子中，简单地重新定位模式匹配是不够的；尝试的定义
getWitness 根本上是不健全的。 （考虑 p 的情况
fun (n : Nat) => n > 0：如果 h 和 h' 是 ∃ x, x > 0 的证明，其中 h 使用
证人 1 和 h' 证人 2，则由于 h = h' 通过证明无关性，得出结论：
getWitness h = getWitness h'—即 1 = 2。）
相反，必须重写 getWitness：函数的结果类型必须是
命题（上面的第一个固定示例），或者 h 一定不是命题（第二个）。
在第一个更正的示例中，useWitness 的结果类型现在是命题 q。这个
允许我们在 h 上进行模式匹配（因为我们要消除为命题类型）并传递
解压后的值为 hq。从程序化的角度来看，可以将 useWitness 视为重写
getWitness 采用连续传递风格，限制后续计算使用其结果
仅根据禁止命题大的要求在 Prop 中构造值
消除。请注意，useWitness 是存在消除原理 Exists.elim。
第二个更正的示例将 h 的类型从存在命题更改为
Type 值依赖对（对应于 PSigma 类型构造函数）。自从
该类型不是命题，消去 α : Type u 不再无效，并且
以前尝试的模式匹配现在进行类型检查。