[Agda] Performance issues and code structure.

[Ulf Norell]

On Mon, Sep 28, 2009 at 12:49 PM, Dan Doel <dan.doel at gmail.com> wrote:

> On Monday 28 September 2009 5:52:29 am Nils Anders Danielsson wrote:
> > Interestingly you get better performance also when you replace {C} with
>
> {?}, but not when {_} is used. I wonder what is going on here. Ulf?
>

That's very strange. The type checker doesn't (shouldn't) care whether it's
a ? or a _. Internally everything is treated as _.


> > 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.
>

It doesn't give you proper proof irrelevance (see
https://lists.chalmers.se/pipermail/agda/2008/000547.html), and it doesn't
work with --type-in-type (there might be problems with
--universe-polymorphism as well, I haven't checked). It might be a good idea
to disable the flag until we have something a bit more robust.


> / Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20090928/f85b6dda/attachment.html