Ada*_*dam 2 coq
可以用Coq中的非建构方式证明存在定理吗？具体而言,我正在考虑证明存在无理数的问题是合理的.
ejg*_*ego 6
对于该特定证明,您将需要假设排除的中间公理.您可以从库中导入它:
Require Import Coq.Logic.Classical_Prop. About classic.
或者以某种特定的形式自己添加(更高级的使用,因为它需要一些小心).尽管如此,标准库中的实数已经是经典的,因此您可以从中推导出这个原理.
归档时间：
9 年 前
查看次数：
139 次
最近记录：