[Agda] Implementation of abstract vs. irrelevance
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...
More information about the Agda