<br><div class="gmail_quote">On Mon, Sep 28, 2009 at 12:49 PM, Dan Doel <span dir="ltr"><<a href="mailto:dan.doel@gmail.com">dan.doel@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im">On Monday 28 September 2009 5:52:29 am Nils Anders Danielsson wrote:<br>
> <span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 13px; border-collapse: collapse; ">Interestingly you get better performance also when you replace {C} with<span class="Apple-style-span" style="border-collapse: separate; font-family: arial; font-size: small; "> </span></span></div>
</blockquote><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div class="im"><span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 13px; border-collapse: collapse; ">> {?}, but not when {_} is used. I wonder what is going on here. Ulf?</span></div>
</blockquote><div><br></div><div>That's very strange. The type checker doesn't (shouldn't) care whether it's a ? or a _. Internally everything is treated as _.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im">> I believe that --proof-irrelevance is broken and should not be used.<br>
> Ulf, can you verify this? If this is true, then the flag should be<br>
> disabled.<br></div></blockquote><div><br></div><div>It doesn't give you proper proof irrelevance (see <a href="https://lists.chalmers.se/pipermail/agda/2008/000547.html">https://lists.chalmers.se/pipermail/agda/2008/000547.html</a>), 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.</div>
<div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div class="im">
</div></blockquote></div>/ Ulf