[Agda] Unsolved metas

[Dominique Devriese]

Permjacov,

2011/2/10 Christoph Herrmann <ch at cs.st-andrews.ac.uk>:
>> When I try to typecheck some of my code in batch mode, Agda reports
>> about unsolved metas and terminates. What does it (unsolved metas) mean
>
> This means the type checker cannot verify type correctness, but also cannot
> construct a contradiction such as zero /= suc

Therefore, what you should try to do is help the typechecker some
more. In the Agda emacs interface, some code will be highlighted in
yellow, indicating where the unsolved metas are located. You should
then try to figure out which arguments it is not able to infer and
provide them manually. Often, all you need is to provide a hidden
argument explicitly, e.g. (id {A = SomeType}) instead of just id.

Dominique