我正在浏览软件基础并遇到错误。
ERROR : The term "true" has type "bool" while it is expected to have type "Datatypes.bool"
下面的证明。
Theorem beq_nat_true : forall n m,
beq_nat n m = true -> n = m.
我发现当我使用Require Import Omega时会发生这种情况。
关于 Omega 向环境中引入什么的任何提示、建议或解释？
最佳答案
Omega 模块间接导入了操作自然数的标准库的许多定义，其中一些最终成为软件基础的影子部分。 beq_nat 函数就是其中之一。出现问题的原因是 beq_nat 的标准库版本返回标准 bool 值，而 SF 的标准库版本返回其重新定义的 bool 值。
我们不久前注意到这个问题，并且已经在 current version 中修复了它。 。如果您不想重新下载所有内容(或者您自己导入了 Omega)，您也可以只限定 beq_nat 使用正确的版本。我的猜测是 Basics.beq_nat 应该可以工作。
关于coq - 需要导入 Omega 后混合了 bool 和 Datatypes.bool，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/36250812/