[Agda] heap mistery

Andrea Vezzosi sanzhiyan at gmail.com
Sat May 21 01:00:54 CEST 2011


I guess there's no way to avoid this problem if the type you're
eliminating is a record though, since pattern matching is desugared to
projections?
If so it'd explain why in some cases I get a big performance
improvement by using a custom record type instead of just nesting
sigmas.


- Andrea


More information about the Agda mailing list