[Agda] how to run helloworld in agda

[Mandy Martino]

Hi Andres,
After meet message  need {-# BUILTIN IO name #-},
i  add  {-# BUILTIN IO name #-} or  {-# BUILTIN IO hello #-}, still have error,
when  and where  need  this?
martin at ubuntu:~/hilbertreborn$ time agda -c hello.agda -i. -iagda-stdlib-0.11/src --ghc-flag=/home/martin/hilbertreborn/agda-prelude/agda-ffi/Agda/FFI.hsChecking hello (/home/martin/hilbertreborn/hello.agda)./home/martin/hilbertreborn/hello.agda:1,16-20Not in scope:  name at /home/martin/hilbertreborn/hello.agda:1,16-20when scope checking name
real	0m0.080suser	0m0.012ssys	0m0.024smartin at ubuntu:~/hilbertreborn$ cat hello.agda{-# BUILTIN IO name #-}open 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 : IO Unitmain = ex

Compiling Relation.Binary.Reflection in /home/martin/hilbertreborn/agda-stdlib-0.11/src/Relation/Binary/Reflection.agdai to /home/martin/hilbertreborn/MAlonzo/Code/Relation/Binary/Reflection.hsRelation.Nullary : no compilation is needed.Compiling Relation.Nullary.Decidable in /home/martin/hilbertreborn/agda-stdlib-0.11/src/Relation/Nullary/Decidable.agdai to /home/martin/hilbertreborn/MAlonzo/Code/Relation/Nullary/Decidable.hsCompiling 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	0m11.462suser	0m5.528ssys	0m4.080s

Regards,
Martin 

> From: asr at eafit.edu.co
> Date: Sat, 19 Dec 2015 07:28:33 -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 07:01, Mandy Martino <tesleft at hotmail.com> wrote:
> > succeed to run an example,  but  got error  +  not  in scope  when follow a
> > web  site,
> >
> > open import Algebra.Structures as A using (IsCommutativeMonoid)
> > open import Data.Nat.Properties using (isCommutativeSemiring)
> >
> 
> Missing modules:
> 
> open import Data.Nat.Base
> open import Relation.Binary.PropositionalEquality
> 
> Please report this error to the author of the Agda tutorial.
> 
> -- 
> Andrés
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151219/2a095c6c/attachment.html