Hello, <br><br>I have a question about the agda&#39;s type checker. <br>I have read that definitions imported from a file won’t need to be rechecked. <br><br>But, when I import a file that takes 36 hours aprox. to checking in another file that takes just seconds to checking (without this import ) the type checker takes hours (I don&#39;t know how many) instead of seconds. I put the .agdai file in the same directory than the second file. <br>
So, ¿why checking the second file takes soo much time when I import other checked file?<br><br>
Thanks, <br>Cecilia<br><br><br>