[Agda] how to run helloworld in agda

[Mandy Martino]

Hi  Andres,
got  error  No binding for builtin thing IO, use {-# BUILTIN IO name #-} tobind it to 'name'
even  if  no  main  ::  IO Unit
Compiling hello in /home/martin/hilbertreborn/hello.agdai to /home/martin/hilbertreborn/MAlonzo/Code/Qhello.hsNo binding for builtin thing IO, use {-# BUILTIN IO name #-} tobind it to 'name'
real	0m4.174suser	0m1.348ssys	0m1.492smartin at ubuntu:~/hilbertreborn$ cat hello.agdamodule hello whereopen import Data.Nat.Baseopen import Relation.Binary.PropositionalEqualityopen import Algebra.Structures as A using (IsCommutativeMonoid)open import Data.Nat.Properties using (isCommutativeSemiring)
open A.IsCommutativeSemiringopen A.IsCommutativeMonoid (+-isCommutativeMonoid isCommutativeSemiring)
ex : ∀ n → (n + 1) + 1 ≡ n + 2ex n = assoc n 1 1
main = ex


Regards,
Martin 

> From: asr at eafit.edu.co
> Date: Sat, 19 Dec 2015 13:08:18 -0500
> Subject: Re: [Agda] how to run helloworld in agda
> To: tesleft at hotmail.com
> CC: agda at lists.chalmers.se
> 
> 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
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151220/2b96e052/attachment.html