代码之家  ›  专栏  ›  技术社区  ›  problème0123

coq我应该用什么战术来对付所有A:Prop,A->~~ A

coq
  •  -2
  • problème0123  · 技术社区  · 7 年前
    内容过于久远，请刷新稍后重试
    2 回复  |  直到 7 年前
        1
  •  7
  •   Anton Trunov    7 年前
        2
  •  0
  •   Carl Patenaude Poulin    7 年前
    推荐文章
    Mei Zhang  ·  定义“依赖类型”模函子
    6 年前
    Jason Hu  ·  参见Ltac中的Hintbase
    6 年前
    lllllllllllll  ·  通过两个实现对阶乘程序进行Coq验证
    6 年前
    MikkelBybjerg  ·  如何延迟lambda评估,以便替换lambda
    6 年前
    user9335697  ·  实例化参数以评估函数定义
    6 年前
    Jian Wang  ·  Coq中的背景目标、搁置目标和放弃目标是什么?
    6 年前
    Pablo Inostroza  ·  有没有可能表达一个定理,说明应用了哪些构造函数?
    6 年前
    jmite  ·  Coq:在校样脚本编写期间查看校样术语
    6 年前
    ConfusedFormalizer  ·  a是怎样的。vo文件的结构是否便于coqchk使用?
    6 年前
    Siddharth Bhat  ·  查看所有已安装的库以及如何在Coq中导入它们
    7 年前
    关于   移动版
    代码之家 - 一站式码农服务社区
    沪ICP备11025650号