<br><div class="gmail_quote">On Mon, Mar 22, 2010 at 11:13 PM, Conor McBride <span dir="ltr"><<a href="mailto:conor@strictlypositive.org">conor@strictlypositive.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi folks<br>
<br>Loading the file and committing that<br>
refinement takes a while: it's done in less than half a minute on<br>
my pathetic-but-thin computer. However (you guessed it) loading<br>
the completed proof just does not want to happen.<br>
<br>But it might also be worth trying to figure out what the reason<br>
for the discrepancy is. I'm sure it's known that it's a problem,<br>
but is it known what problem it is?</blockquote><div><br></div><div>I just had a quick look and it's termination checking that takes most</div><div>of the time when reloading. We don't do termination checking after a</div>
<div>refinement (maybe we should), so that's why refining the goal works</div><div>and not reloading. It seems that the reason for it taking so long is that</div><div>the term you give is massive after all the implicit arguments are in</div>
<div>place.</div><div><br></div><div>/ Ulf</div></div>