<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:新細明體
}
--></style></head>
<body class='hmmessage'><div dir='ltr'><font size="3" style="font-size:12pt;" color="#000000">Hi Andres,</font><div><br></div><div><font size="3" style="font-size:12pt;" color="#000000">succeed to compile </font></div><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font size="3" style="font-size:12pt;" color="#000000">when the way in </font><a href="http://mazzo.li/posts/AgdaSort.html" target="_blank" style="font-size: 12pt;">http://mazzo.li/posts/AgdaSort.html</a></div><div><font size="3" style="font-size:12pt;" color="#000000">after it has error ambigous name sym, i change to sym1, but i do not understand why it return error repeated variables in pattern</font></div><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font color="#000000"><div>/home/martin/hilbertreborn/hello.agda:14,1-19</div><div>Repeated variables in pattern: refl1</div><div>when scope checking the left-hand side trans1 refl1 refl1 in the</div><div>definition of trans1</div></font><br><div>module hello where</div><div>open import Data.Nat.Base</div><div>open import Relation.Binary.PropositionalEquality</div><div>open import Algebra.Structures as A using (IsCommutativeMonoid)</div><div>open import Data.Nat.Properties using (isCommutativeSemiring)</div><div><br></div><div>open A.IsCommutativeSemiring</div><div>open A.IsCommutativeMonoid (+-isCommutativeMonoid isCommutativeSemiring)</div><div><br></div><div>sym1 : ∀ {X} {x y : X} → x ≡ y → y ≡ x</div><div>sym1 refl1 = refl1</div><div><br></div><div>trans1 : ∀ {X} {x y z : X} → x ≡ y → y ≡ z → x ≡ z</div><div>trans1 refl1 refl1 = refl1</div><div><br></div><div>equivalence1 : ∀ {X} → Equivalence {X} _≡_</div><div>equivalence1 = record { refl1 = refl1; sym1 = sym1; trans1 = trans1 }</div><div><br></div><div>cong1 : ∀ {X} {x y : X} → (f : X → X) → x ≡ y → f x ≡ f y</div><div>cong1 _ refl1 = refl1</div><div><br></div><div>ex : ∀ n → (n + 1) + 1 ≡ n + 2</div><div>ex n = assoc n 1 1</div><div><br></div><div>main = ex</div><br><div>Regards,</div><div><br></div><div>Martin </div><br><br><div>> From: asr@eafit.edu.co<br>> Date: Wed, 23 Dec 2015 20:08:19 -0500<br>> Subject: Re: [Agda] how to run helloworld in agda<br>> To: tesleft@hotmail.com<br>> CC: agda@lists.chalmers.se<br>> <br>> On 23 December 2015 at 14:30, Mandy Martino <tesleft@hotmail.com> wrote:<br>> > i follow the instruction to set, but got error , another command is in<br>> > progress,<br>> > where is wrong?<br>> <br>> You followed the instructions for the development version of Agda but<br>> you aren't using that version.<br>> <br>> <br>> -- <br>> Andrés<br></div></div> </div></body>
</html>