<html>
<head>
<meta content="text/html; charset=UTF-8" http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
I have difficulty reproducing the error. Using a recent version of
Agda (from Apr 13) and using the latest master version of the
standard-library, Agda reports this error:<br>
<br>
code:<br>
<blockquote type="cite"> data _≤″_ (ω : Ω) : Ω → Set where<br>
</blockquote>
message:<br>
<blockquote type="cite">Multiple definitions of _≤″_. </blockquote>
<br>
And when the end of this line is uncommented,<br>
<blockquote type="cite"> open import Data.Nat -- using (ℕ ; zero ;
suc ; _+_ ; _<′_ ; fold)<br>
</blockquote>
<br>
Agda reports this error:<br>
<br>
code:<br>
<blockquote type="cite"> incX-x,Sy : ∀ x y → incΩ x (x , suc y) ≡
zero , suc (y + x)<br>
</blockquote>
message:<br>
<blockquote type="cite">Could not parse the application<br>
incΩ x (x , suc y) ≡ zero , suc (y + x)<br>
</blockquote>
<br>
<br>
<br>
<br>
<div class="moz-cite-prefix">On 04/16/2016 03:34 PM, Serge Leblanc
wrote:<br>
</div>
<blockquote cite="mid:5712BE11.2040505@gmail.com" type="cite">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
Estimata,<br>
<br>
Kial la tipa kontrolilo ne uzas mian antaŭan pruvon 'incX≡' por
unuaigi la tipon ⟨ incΩ (y + x) (suc″ (x , y)) ⟩ kun ⟨ suc x , y ⟩
?<br>
Ĉu ekzistas metodo por fari tion?<br>
Why the type checker don't use my previous proof 'incX≡' for unify
the type ⟨incΩ (y + x) (suc "(x, y))⟩ with ⟨suc x, y⟩?<br>
Is there a method to do this? <span id="result_box" class=""
lang="en"><span class=""><br>
<br>
Sinceran antaŭan dankon.<br>
</span></span>-- <br>
<div class="moz-signature">Serge Leblanc
<hr> gpg --keyserver hkp://keyserver.ubuntu.com:11371
--recv-keys 0x67B17A3F <br>
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>