[Agda] how to run helloworld in agda

[Mandy Martino]

Hi  Andres,i succeed to run an example,  but  got error  +  not  in scope  when follow a web  site,  Any more need to import  or  what syntax  is  error ?/home/martin/hilbertreborn/hello.agda:7,15-16Not in scope:  + at /home/martin/hilbertreborn/hello.agda:7,15-16when scope checking +real	0m3.857suser	0m2.056ssys	0m0.856stime agda -c hello.agda -i. -iagda-stdlib-0.11/src --ghc-flag=/home/martin/hilbertreborn/agda-prelude/agda-ffi/Agda/FFI.hsopen 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 1main = exhttp://people.inf.elte.hu/divip/AgdaTutorial/Application.Algebra.htmlRegards,Martin 
> From: asr at eafit.edu.co
> Date: Sat, 19 Dec 2015 06:43:14 -0500
> Subject: Re: [Agda] how to run helloworld in agda
> To: tesleft at hotmail.com
> 
> Hi Mandy,
> 
> Please resend the question to Agda users mailing list.
> 
> Best.
> 
> 
> On 19 December 2015 at 06:27, Mandy Martino <tesleft at hotmail.com> wrote:
> > Hi,
> >
> > i succeed to run an example,  but  got error  +  not  in scope  when follow
> > a web  site,
> > Any more need to import  or  what syntax  is  error ?
> >
> > /home/martin/hilbertreborn/hello.agda:7,15-16
> > Not in scope:
> >   + at /home/martin/hilbertreborn/hello.agda:7,15-16
> > when scope checking +
> >
> > real 0m3.857s
> > user 0m2.056s
> > sys 0m0.856s
> >
> > time agda -c hello.agda -i. -iagda-stdlib-0.11/src
> > --ghc-flag=/home/martin/hilbertreborn/agda-prelude/agda-ffi/Agda/FFI.hs
> >
> > open import Algebra.Structures as A using (IsCommutativeMonoid)
> > open import Data.Nat.Properties using (isCommutativeSemiring)
> >
> > open A.IsCommutativeSemiring
> > open A.IsCommutativeMonoid (+-isCommutativeMonoid isCommutativeSemiring)
> >
> > ex : ∀ n → (n + 1) + 1 ≡ n + 2
> > ex n = assoc n 1 1
> >
> > main = ex
> >
> >
> > http://people.inf.elte.hu/divip/AgdaTutorial/Application.Algebra.html
> >
> >
> > Regards,
> >
> > Martin
> >
> >
> >> From: asr at eafit.edu.co
> >> Date: Sat, 19 Dec 2015 05:46:11 -0500
> >> Subject: Re: [Agda] how to run helloworld in agda
> >> To: tesleft at hotmail.com
> >>
> >> On 19 December 2015 at 05:39, Mandy Martino <tesleft at hotmail.com> wrote:
> >> > MAlonzo/Code/Agda/Primitive.hs:4:18:
> >> > Could not find module `Agda.FFI'
> >> > Use -v to see a list of the files searched for.
> >>
> >> From agda-stdlib README.agda:
> >>
> >> -- To compile the library using the MAlonzo compiler you first need to
> >> -- install some supporting Haskell code, for instance as follows:
> >> --
> >> -- cd ffi
> >> -- cabal install
> >>
> >>
> >> --
> >> Andrés
> >
> >
> > "La información contenida en este correo electrónico está dirigida
> > únicamente a su destinatario y puede contener información confidencial,
> > material privilegiado o información protegida por derecho de autor. Está
> > prohibida cualquier copia, utilización, indebida retención, modificación,
> > difusión, distribución o reproducción total o parcial. Si usted recibe este
> > mensaje por error, por favor contacte al remitente y elimínelo. La
> > información aquí contenida es responsabilidad exclusiva de su remitente por
> > lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje
> > contenga."
> >
> > "The information contained in this email is addressed to its recipient only
> > and may contain confidential information, privileged material or information
> > protected by copyright. Its prohibited any copy, use, improper retention,
> > modification, dissemination, distribution or total or partial reproduction.
> > If you receive this message by error, please contact the sender and delete
> > it. The information contained herein is the sole responsibility of the
> > sender therefore Universidad EAFIT is not responsible for what the message
> > contains."
> 
> 
> 
> -- 
> Andrés
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151219/a21719b7/attachment.html