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

[Andreas Abel]

If you want to /compile/ an agda file, it has to have a

   main : IO Unit

However, I see no reason to compile your file below, as it has no 
executable code.  It is sufficient to /typecheck/ it.

--Andreas

On 02.01.2016 07:45, Mandy Martino wrote:
> Hi,
>
> No binding for builtin thing IO, use {-# BUILTIN IO name #-} to
> bind it to 'name'
>
> module PropositionalEquality where
>
> data Empty : Set where
> absurd : {X : Set} → Empty → X
> absurd ()
>
> 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 ≡ x
> sym refl = refl
>
> trans : ∀ {X} {x y z : X} → x ≡ y → y ≡ z → x ≡ z
> trans 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 y
> cong _ refl = refl
>
> main = Empty
>
> Regards,
>
> Martin
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/