我正在阅读Mike Nahas 的 Coq 入门教程，其中说：
“ex_intro”的参数是：
我在看定义:
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
ex_intro : forall x:A, P x -> ex (A:=A) P.
我在解析它时遇到困难。表达式的哪些部分forall x:A, P x -> ex (A:=A) P对应于这三个论点（谓词、证人和证明）？
要理解 Mike 的意思，最好启动 Coq 解释器并查询ex_intro:
Check ex_intro.
然后您应该看到：
ex_intro
: forall (A : Type) (P : A -> Prop) (x : A), P x -> exists x, P x
这说的是ex_intro不仅需要 3 个参数，还需要 4 个参数：
- 您要量化的事物的类型，
A;
- 谓词
P : A -> Prop;
- 证人
x : A; and
- 的证明
P x，断言x是有效证人。
如果你把所有这些东西结合起来，你就会得到一个证明exists x : A, P x。例如，@ex_intro nat (fun n => n = 3) 3 eq_refl是一个证明exists n, n = 3.
因此，实际类型之间的差异ex_intro您在定义中读到的内容是，前者包含标头中给出的所有参数 - 在本例中，A and P.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
