[Agda] how to run helloworld in agda

[Mandy Martino]

Hi Andres,
succeed to compile  
when the  way  in  http://mazzo.li/posts/AgdaSort.htmlafter  it  has  error  ambigous name  sym,  i change  to sym1,  but  i do not understand  why  it  return  error  repeated  variables in pattern
/home/martin/hilbertreborn/hello.agda:14,1-19Repeated variables in pattern: refl1when scope checking the left-hand side trans1 refl1 refl1 in thedefinition of trans1
module 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)
sym1 : ∀ {X} {x y : X} → x ≡ y → y ≡ xsym1 refl1 = refl1
trans1 : ∀ {X} {x y z : X} → x ≡ y → y ≡ z → x ≡ ztrans1 refl1 refl1 = refl1
equivalence1 : ∀ {X} → Equivalence {X} _≡_equivalence1 = record { refl1 = refl1; sym1 = sym1; trans1 = trans1 }
cong1 : ∀ {X} {x y : X} → (f : X → X) → x ≡ y → f x ≡ f ycong1 _ refl1 = refl1
ex : ∀ n → (n + 1) + 1 ≡ n + 2ex n = assoc n 1 1
main = ex
Regards,
Martin 

> From: asr at eafit.edu.co
> Date: Wed, 23 Dec 2015 20:08:19 -0500
> Subject: Re: [Agda] how to run helloworld in agda
> To: tesleft at hotmail.com
> CC: agda at lists.chalmers.se
> 
> On 23 December 2015 at 14:30, Mandy Martino <tesleft at hotmail.com> wrote:
> > i follow the instruction to set, but got  error , another command  is  in
> > progress,
> > where is  wrong?
> 
> You followed the instructions for the development version of Agda but
> you aren't using that version.
> 
> 
> -- 
> Andrés
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160101/c5ab7448/attachment.html