Agda Standart Kitaplığı yükleniyor

Question

Agda'yı (sürüm 2.3.2.2) ve Standart Kitaplığı'nı (sürüm 0.7) yükledim.
Standart Kitaplığı almayan programı yükleyebilirim.
Örneğin, ben Standart Kütüphanesi yüklediğinizde, ben hata altına aldık

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

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

yükleyemez, ancak

data Bool : Set where 
true : Bool 
false : Bool 

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

yükleyebilirsiniz.

/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 

Hataları düzeltmek için herhangi bir fikir?

Answer 1

Bu sürümlerden emin misiniz? 2.3.2.2, 0.7 ile uyumlu olmalıdır. Agda'nızın 2.3.2.2'den daha yeni olduğu gibi görünüyor. ...\Agda-2.3.2.2\lib\prim\Agda\Primitive.agda dosya var mı? Orada olmamalı.

Bu yöntem işe yaramazsa, el Buna Level modülün içeriğini değiştirmek için deneyebilirsiniz:

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 

Ama diğer sorunları olasılıkla karşılaşırsınız.

Gerçekten Agda ve stdlib'in eski sürümlerini istiyor musunuz?