<!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">&lt;permeakra@gmail.com&gt;</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">&lt;dominique.devriese@gmail.com&gt;</a></td>
        </tr>
      </tbody>
    </table>
    <br>
    <br>
    <pre>On 02/10/2011 02:41 PM, Dominique Devriese wrote:
&gt; Permjacov,
&gt;
&gt; 2011/2/10 Christoph Herrmann <a class="moz-txt-link-rfc2396E" href="mailto:ch@cs.st-andrews.ac.uk">&lt;ch@cs.st-andrews.ac.uk&gt;</a>:
&gt;&gt;&gt; When I try to typecheck some of my code in batch mode, Agda reports
&gt;&gt;&gt; about unsolved metas and terminates. What does it (unsolved metas) mean
&gt;&gt; This means the type checker cannot verify type correctness, but also cannot
&gt;&gt; construct a contradiction such as zero /= suc
&gt; Therefore, what you should try to do is help the typechecker some
&gt; more. In the Agda emacs interface, some code will be highlighted in
&gt; yellow, indicating where the unsolved metas are located. You should
&gt; then try to figure out which arguments it is not able to infer and
&gt; provide them manually. Often, all you need is to provide a hidden
&gt; argument explicitly, e.g. (id {A = SomeType}) instead of just id.
&gt;
&gt; Dominique
&gt; _______________________________________________
&gt; Agda mailing list
&gt; <a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
&gt; <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>