[Agda] Implementation of abstract vs. irrelevance

[Andrea Vezzosi]

Hi,

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?


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