coq
-
什么都不做的战术是什么？
-
如何在 Ltac 中尝试策略，但如果失败则继续
-
COQ 中子序列的传递性
-
在 Coq 中，CoInductive "extensionality" 是正确的吗？它具有普遍性吗？
-
单例中的隐式参数 class
-
Set 与 Prop 的可判定相等性声明
-
Coq 中的实数
-
为什么 "only printing" 符号会修改解析器
-
如何在 Coq/ 中对 BinNums.Z 进行归纳
-
Coq Error: Illegal application (Non-functional construction)
-
在 Coq 中使用构造函数中的命名参数进行证明
-
证明 s-expressions 打印是单射的
-
如何应用公理来简化 Coq 中的匹配？
-
任何人都可以帮助我如何在 coq 中证明这个定理
-
软件基础：weak_pumping 引理证明
-
不漂亮地打印记录的字段
-
证明中生成的奇怪目标“Some 0 = true”
-
在 Coq 中如何表达归纳关系的一个元素不能从另一个元素推导出来？
-
如何证明定理 plus_lt : forall n1 n2 m, n1 + n2 < m -> n1 < m /\ n2 < m
-
如何证明 `plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m.`