coq
-
证明包含不存在的定理
-
这个 Coq 定理有更短的证明吗？
-
Coq：关系组合的关联性
-
这两个证明是等价的吗？
-
在 Coq 中反转向量
-
CoqIde中如何导入Coq库HoTT
-
无法启动 CoqIde
-
我如何在 Coq 中证明 0 <= a < b -> r a b = a？
-
Coq：一个有两个相同子目标的恶性循环
-
如何在 Coq 中重新排序存在变量？
-
Info 白话命令如何工作？
-
比较树的相互递归函数
-
有没有更优雅的方法让 coq 相信基于列表的假设是矛盾的？
-
证明助手中的认证计算
-
Coq 似乎拒绝承认命题公式对命题变量的简单替换？
-
如何用某个 属性 的术语替换某个术语？
-
是否可以在 Coq 中声明类型相关的表示法？
-
Coq 中 HOL 式 alpha 转换的统一问题（匹配等式）
-
Kami（Bluespec 的 Coq 框架）能够在 WSL Ubuntu 上 运行 的正确设置是什么？
-
`induction n, m` 和 `induction n; 有什么区别？ Coq 中的感应 m`？