[Agda] Implementation of abstract vs. irrelevance

Andrea Vezzosi sanzhiyan at gmail.com
Sun May 12 12:00:23 CEST 2013


I've noticed some very promising speedups by making definitions abstract in
addition to irrelevant and I'd like to understand why.

Skimming the code I couldn't figure out where the main pieces of the
implementation of these features are, is there a commentary on how they are
implemented? And what work does abstract save on top of irrelevance?

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130512/c4f4b568/attachment.html

More information about the Agda mailing list