The Coq mailing list

["Floyd Lee" <undecidable AT secureroot.com>]

--- 
guillaume.brunerie AT gmail.com
 wrote:
> There is no definitional eta for pairs in Coq 8.4, only for functions.
> In particular the term  let (y, z) := f x in (y, z)  is not
> definitionally equal to (f x), only propositionally.

Ah, I see.

Do you happen to know if it's safe to assume eta_let_pair_eq as an axiom?


_____________________________________________________________
---
http://mail.secureroot.com/ - free mailbox for hackers and geeks