[Agda] heap mistery

[Andreas Abel]

Hello Martin and Andrea,

when I will be less loaded with teaching and referee obligations and 
deadlines next time, I will have a look on how to deal with the 
(superfluous) normalization during unification.  That hopefully will fix 
your problem, Martin.  Your test case will be very useful for debugging 
the performance problems.

Cheers,
Andreas

On 21.05.11 1:00 AM, Andrea Vezzosi wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/