[Agda] ordering uniqueness

Marco Maggesi maggesi at math.unifi.it
Fri Oct 11 15:28:21 CEST 2013


>From what you say, it seems a similar problem, indeed.
Sometimes changing the datatype representation can be proficuous.
But this not always true, of course.  In particular, whenever you use
McBride-MkKinna
views you are working intrinsically with the "wrong" representation.
(Otherwise why use a view?)  Therefore I think that this kind of situations
are destined to happen regularly.

Marco
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131011/682acca9/attachment.html


More information about the Agda mailing list