1
我安裝了Agda(版本2.3.2.2)和標準庫(版本0.7)。
我可以加載不導入標準庫的程序。
例如,我可以加載加載Agda的標準庫
data Bool : Set where
true : Bool
false : Bool
not : Bool -> Bool
not false = true
not true = false
但是,我無法加載
open import Data.Bool
data Bool : Set where
true : Bool
false : Bool
not : Bool -> Bool
not false = true
not true = false
當我加載標準庫,我得到了下面的錯誤。
/Users/my_name/.cabal/share/Agda-2.3.2.2/lib-0.7/src/Level.agda:27,1-32
Duplicate binding for built-in thing LEVEL, previous binding to.Agda.Primitive.Level
when checking the pragma BUILTIN LEVEL Level
任何想法來解決錯誤?
Agda的版本不是2.3.2.2!對不起,謝謝!我可以加載圖書館! – mmsss