我可以看到Coq用于定义引理的不同语法。例如,Lemma plus_n_O: forall n:nat, n = n + 0.
和Lemma plus_n_O n: n = n + 0.
都定义了零与任意数字之和等于该数字。这些定义有何不同?或者,这是Coq的一个新特性,可以从定义中删除forall
量词。
发布于 2019-06-13 04:39:25
这两个定义在本质上是等价的。一般而言,任何形式的语句
Lemma foo x y z : P.
Proof.
(* ... *)
等同于
Lemma foo : forall x y z, P.
Proof.
intros x y z.
(* ... *)
https://stackoverflow.com/questions/56570004
复制相似问题