[Agda] Performance issues and code structure.

[Nils Anders Danielsson]

On 2009-09-28 09:38, Dan Doel wrote:
> This is the version that performs acceptably with all the proofs. The version 
> that was using all my memory and then overflowing the stack omitted those two 
> {C}s when opening _Product.

Interestingly you get better performance also when you replace {C} with
{?}, but not when {_} is used. I wonder what is going on here. Ulf?

> [...] --proof-irrelevance [...]

I believe that --proof-irrelevance is broken and should not be used.
Ulf, can you verify this? If this is true, then the flag should be
disabled.

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.