[Agda] how to run helloworld in agda

[Andrés Sicard-Ramírez]

On 19 December 2015 at 08:06, Mandy Martino <tesleft at hotmail.com> wrote:
> After meet message  need {-# BUILTIN IO name #-},
>
> i  add  {-# BUILTIN IO name #-} or  {-# BUILTIN IO hello #-}, still have
> error,
>
> when  and where  need  this?

See http://agda.readthedocs.org/en/latest/language/built-ins.html#io .

You can use the IO from the standard library as I showed in an previous example.

> ex : ∀ n → (n + 1) + 1 ≡ n + 2
> ex n = assoc n 1 1
>
> main : IO Unit
> main = ex

Since `ex` hasn't type `IO Unit` you'll get a type error.


-- 
Andrés