<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=ISO-8859-1">
</head>
<body bgcolor="#ffffff" text="#000000">
<br>
<br>
-------- Original Message --------
<table class="moz-email-headers-table" border="0" cellpadding="0"
cellspacing="0">
<tbody>
<tr>
<th align="RIGHT" valign="BASELINE" nowrap="nowrap">Subject: </th>
<td>Re: [Agda] Unsolved metas</td>
</tr>
<tr>
<th align="RIGHT" valign="BASELINE" nowrap="nowrap">Date: </th>
<td>Thu, 10 Feb 2011 15:23:07 +0300</td>
</tr>
<tr>
<th align="RIGHT" valign="BASELINE" nowrap="nowrap">From: </th>
<td>Permjacov Evgeniy <a class="moz-txt-link-rfc2396E" href="mailto:permeakra@gmail.com"><permeakra@gmail.com></a></td>
</tr>
<tr>
<th align="RIGHT" valign="BASELINE" nowrap="nowrap">To: </th>
<td>Dominique Devriese <a class="moz-txt-link-rfc2396E" href="mailto:dominique.devriese@gmail.com"><dominique.devriese@gmail.com></a></td>
</tr>
</tbody>
</table>
<br>
<br>
<pre>On 02/10/2011 02:41 PM, Dominique Devriese wrote:
> Permjacov,
>
> 2011/2/10 Christoph Herrmann <a class="moz-txt-link-rfc2396E" href="mailto:ch@cs.st-andrews.ac.uk"><ch@cs.st-andrews.ac.uk></a>:
>>> 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
> <a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
> <a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
Yep, that helped. However, that was real pain. Thanks.
</pre>
</body>
</html>