<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
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">michel.levy.imag@free.fr</a> <br>
mobile : 06 59 13 42 53<br>
web : michel.levy.imag.free.fr
</div>
</body>
</html>