<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Use _,'_ instead - it is the non-dependent version. proj1 works
because you're declaring B to not depend on A, but in general _,_
is dependent.</p>
<p>Jacques<br>
</p>
<div class="moz-cite-prefix">On 2020-04-18 4:18 p.m., Michel Levy
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:c4ae132d-8911-982c-1fd3-2b6518cac884@free.fr">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
I have a problem with the two lines below in the context <br>
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_
to ⟨_,_⟩)<br>
<p>test0 : 1 ≡ proj₁ ⟨ 1 , 2 ⟩<br>
test0 = refl</p>
<p>———— Errors ————————————————————————————————————————————————<br>
Failed to solve the following constraints:<br>
_50 := 2 [blocked on problem 99]<br>
[99] ℕ =< _B_49 1 : Set</p>
<p>The term proj₁ ⟨ 1 , 2 ⟩ appears in <u>yellow</u> and its
value calculated by C-c C-n is 1</p>
<p><br>
</p>
<p>Still more strange, when I rename proj₁ in proj1 with <br>
</p>
<p>proj1 : {A B : Set} -> A × B -> A<br>
proj1 ⟨ x , y ⟩ = x<br>
</p>
<p>I have without error</p>
<p>test0' : 1 ≡ proj1 ⟨ 1 , 2 ⟩<br>
test0' = refl<br>
</p>
<div class="moz-signature">-- <br>
courriel : <a class="moz-txt-link-abbreviated"
href="mailto:michel.levy.imag@free.fr" moz-do-not-send="true">michel.levy.imag@free.fr</a>
<br>
mobile : 06 59 13 42 53<br>
web : michel.levy.imag.free.fr </div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-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>
</body>
</html>