[Agda] Proving equality of pairs

David Leduc david.leduc6 at googlemail.com
Fri Sep 24 17:09:48 CEST 2010


> -- (or define a cartesian product type instead of using the library's sigma
> types)

It seems that _x_ should not be defined the way it is in the standard library.


More information about the Agda mailing list