<div dir="ltr">Thanks for your reply!<div><br></div><div>Yes, that is the case. The copied versions now share the definition of "lAssoc" and "rAssoc".</div></div><div class="gmail_extra"><br><div class="gmail_quote">2017-06-13 11:39 GMT+01:00 Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 2017-06-13 11:44, Jan Bracker wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I have got around the issue of the compilation possibly not<br>
terminating by simply copying the definition of "fca" and "fca'" into<br>
the module with the holes. Now it takes about 40 seconds to compile.<br>
<br>
Can anybody explain why just importing these definitions from another<br>
module causes this horrible increase in compilation time? I always<br>
thought separating Agda proofs into several modules was the best way<br>
to decrease compilation time.<br>
</blockquote>
<br></span>
When you used two modules you had two definitions of lAssoc/rAssoc. I'm<br>
guessing that, when you copied the definitions of fca and fca', you<br>
arranged things so that they shared the definitions of lAssoc/rAssoc<br>
with the type signature "NaturalTransformation lAssoc rAssoc".<br>
<br>
Agda's convertibility check has a special case for terms that are<br>
syntactically identical. My guess is that this special case was<br>
triggered in the latter case, but not in the former, and that some<br>
reduction was triggered in the former case. (But this is just a guess.)<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
</font></span></blockquote></div><br></div>