[Agda] type checker

[Nils Anders Danielsson]

On 2011-12-05 13:10, Cecilia Manzino wrote:
> I have a question about the agda's type checker. I have read that
> definitions imported from a file won’t need to be rechecked.
>
> 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't know how many) instead of
> seconds. I put the .agdai file in the same directory than the second
> file. So, ¿why checking the second file takes soo much time when I
> import other checked file?

It sounds as if the first file is checked again. To see if this is the
case you can use the command-line program. If it prints "Checking"
rather than "Skipping", then the file is checked again.

This can have several causes. For instance, the time stamps of the files
may have changed, or perhaps you have upgraded Agda.

-- 
/NAD