在需要導入之後混合使用bool和Datatypes.bool

Question

我正在瀏覽軟件基礎並遇到錯誤。

ERROR：術語「真」具有同時預計將有型「Datatypes.bool」

下面的隔爆型「布爾」。

Theorem beq_nat_true : forall n m, 
    beq_nat n m = true -> n = m. 

我發現在使用Require Import Omega時發生了這種情況。
Omega引入環境的任何提示，建議或解釋？

Answer 1

Omega模塊間接導入了操縱自然數的標準庫的許多定義，其中一些定義了軟件基礎的陰影部分。 beq_nat函數就是其中之一。問題出現是因爲beq_nat的標準庫版本返回標準布爾值，而SF中的一個返回其重新定義的布爾值。

我們剛纔注意到了這個問題，並且已經在current version中修復了它。如果您不想重新下載所有內容（或者您自己導入了Omega），那麼您也可以僅限於beq_nat使用正確的版本。我的猜測是Basics.beq_nat應該工作。