[Agda] problem with proj1

[Jacques Carette]

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.

Jacques

On 2020-04-18 4:18 p.m., Michel Levy wrote:
> I have a problem with the two lines below in the context
> open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
>
> test0 : 1 ≡ proj₁ ⟨ 1 , 2 ⟩
> test0 = refl
>
> ———— Errors ————————————————————————————————————————————————
> Failed to solve the following constraints:
>   _50 := 2 [blocked on problem 99]
>   [99] ℕ =< _B_49 1 : Set
>
> The term proj₁ ⟨ 1 , 2 ⟩ appears in _yellow_ and its value calculated 
> by C-c C-n is 1
>
>
> Still more strange, when I rename proj₁ in proj1 with
>
> proj1 : {A B : Set} -> A × B -> A
> proj1 ⟨ x , y ⟩ = x
>
> I have without error
>
> test0' : 1 ≡ proj1 ⟨ 1 , 2 ⟩
> test0' = refl
>
> -- 
> courriel : michel.levy.imag at free.fr
> mobile : 06 59 13 42 53
> web : michel.levy.imag.free.fr
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200418/3fd7b669/attachment.html>