2016-04-09 61 views
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 

任何想法來解決錯誤?

回答

2

您確定這些版本? 2.3.2.2應該與0.7兼容。它看起來像你的Agda比2.3.2.2更新。是否有...\Agda-2.3.2.2\lib\prim\Agda\Primitive.agda文件?它不應該在那裏。

如果沒有幫助,您可以嘗試將Level模塊的內容手動改成這樣:

module Level where 

-- Levels. 

open import Agda.Primitive public 
    using (Level; _⊔_) 
    renaming (lzero to zero; lsuc to suc) 

-- Lifting. 

record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where 
    constructor lift 
    field lower : A 

open Lift public 

但你很可能會遇到其他問題。

你真的想要舊版本的Agda和stdlib嗎?

+0

Agda的版本不是2.3.2.2!對不起,謝謝!我可以加載圖書館! – mmsss