[Agda] with x =? x

Andrea Vezzosi sanzhiyan at gmail.com
Wed Dec 31 23:43:22 CET 2014


Ah, yeah, for setoids you are going to want to prove something more
general, just that there exists some proof that makes them equal,
rather than insisting it's ≈refl.


More information about the Agda mailing list