[Agda] No binding for builtin thing IO, use {-# BUILTIN IO name #-} to bind it to 'name'

[Mandy Martino]

Hi,
No binding for builtin thing IO, use {-# BUILTIN IO name #-} tobind it to 'name'
module PropositionalEquality where
data Empty : Set whereabsurd : {X : Set} → Empty → Xabsurd ()
infix 3 ¬_¬_ : Set → Set¬ X = X → Empty
Rel : Set → Set₁Rel X = X → X → Set
record Equivalence {X} (_≈_ : Rel X) : Set₁ where  field    refl  : ∀ {x}     → x ≈ x    sym   : ∀ {x y}   → x ≈ y → y ≈ x    trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
data _≡_ {X} : Rel X where    refl : ∀ {x} → x ≡ x
sym : ∀ {X} {x y : X} → x ≡ y → y ≡ xsym refl = refl
trans : ∀ {X} {x y z : X} → x ≡ y → y ≡ z → x ≡ ztrans refl refl = refl
equivalence : ∀ {X} → Equivalence {X} _≡_equivalence = record { refl = refl; sym = sym; trans = trans }
cong : ∀ {X} {x y : X} → (f : X → X) → x ≡ y → f x ≡ f ycong _ refl = refl
main = Empty
Regards,
Martin 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160102/e314a131/attachment.html