用于定义引理的Coq语法
用于定义引理的Coq语法
提问于 2019-06-13 04:35:35
我可以看到Coq用于定义引理的不同语法。例如，Lemma plus_n_O: forall n:nat, n = n + 0.和Lemma plus_n_O n: n = n + 0.都定义了零与任意数字之和等于该数字。这些定义有何不同？或者，这是Coq的一个新特性，可以从定义中删除forall量词。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/56570004
复制相关文章
相似问题