[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