coq-tactic
-
使用 coq 反转策略的矛盾假设
-
在 Coq 中用匹配表达式分解构造函数的相等性
-
coq tactics语言中，intro和intros有什么区别
-
Coq 命令 Require Import Ltac 有什么作用？
-
ltac：可选变量名
-
Coq CompCert 中的 EvalOp 是什么
-
参考 Ltac 中的 hintbases
-
`match` 能比 `rewrite` 快吗
-
Coq：当我们有很多等式时控制 `subst`
-
在 Coq 中加入记录成员？
-
我可以在 "coqtop - nois" 下定义战术吗？
-
如何证明关于对列表的定理
-
在 <Hypothesis>` 模式中使用 `<tactic> 用于用户定义的策略
-
在 coq 中推导模式匹配的事实
-
Coq 中相互递归类型的“决定相等性”？
-
Coq 中内置策略（case、destruct、inversion 等）的确切定义
-
Coq中相等类型证据的案例分析
-
Coq：自动重复重写
-
让“自动”执行案例分析的惯用方法是什么？
-
"functional induction" 策略在 Coq 中有什么作用？