Agda標準ライブラリの読み込み

Question

Agda（バージョン2.3.2.2）と標準ライブラリ（バージョン0.7）がインストールされました。
標準ライブラリをインポートしないプログラムを読み込むことができます。
例えば、私は標準ライブラリをロードすると、私はエラーの下になった

open import Data.Bool 
data Bool : Set where 
true : Bool 
false : Bool 

not : Bool -> Bool 
not false = true 
not true = false 

ロードすることはできません、しかし

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 

エラーを解決する方法はありますか？

Answer 1

バージョンについて確認してください。 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が必要ですか？