Fwd: Re: [Agda] Unsolved metas

[Permjacov Evgeniy]

-------- Original Message --------
Subject: 	Re: [Agda] Unsolved metas
Date: 	Thu, 10 Feb 2011 15:23:07 +0300
From: 	Permjacov Evgeniy <permeakra at gmail.com>
To: 	Dominique Devriese <dominique.devriese at gmail.com>



On 02/10/2011 02:41 PM, Dominique Devriese wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
Yep, that helped. However, that was real pain. Thanks.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110210/c75c7093/attachment.html