<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 7, 2013 at 2:30 PM, Nils Anders Danielsson &lt;<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>&gt; wrote:<br><br>    On 2013-11-07 13:43, Carlos Camarao wrote:<br>
<br>        The documentation (from<br>        <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Auto">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Auto</a>) is not<br>        very clear about auto&#39;s behavior:<br>
<br>        &quot;Search parameters are given by entering them into the hole before<br>        invocation. Giving no arguments is fine and results in a search with<br>        default parameters. The search carries on until either a solution is<br>
        found, the search space is fully (and unsuccessfully) explored or it<br>        times out (5 seconds by default). Here follows a list of the different<br>        modes and parameters. ...&quot;<br><br>        I had not read this, but even if I had, I could interpret &quot;a solution&quot;<br>
        (in &quot;The search carries on until either a solution...&quot; above) as<br>        &quot;a unique solution&quot;: I think this is what auto should do unless<br>        otherwise explicitly indicated. <br><br>    I&#39;ve modified the text on the wiki:<br>
<br>      &quot;The search carries on until either a (not necessarily unique)<br>      solution is found, ...&quot;<br><br>    If Agda&#39;s unifier instantiates a meta-variable with a non-unique<br>    solution, then this is a bug. However, C-c C-a is allowed to find<br>
    non-unique solutions.<br><br>Thanks a lot.<br><br>I&#39;d suggest to include a -u &quot;parameter&quot;, to allow a unique solution to be searched. <br>And also perhaps highlight the issue by modifying the wiki, right at the 1st paragraph, <br>
as follows:<br><br>===================<br>Auto<br><br>Agda supports (since version 2.2.6) command ‘Auto’, that performs a<br>search for a type inhabitant, which is then used to fill a hole.<br><br>The existence of a unique type inhabitant can be specified, <br>
via parameter -u (read about parameters below).<br><br>Auto can be used as an aid when interactively ... <br><br>Usage<br>... <br>Here follows a list of the different modes and parameters.<br>...<br>Listing and selecting solutions<br>
<br>By default, Auto replaces the hole with the first solution found. <br><br>Parameter -u can change this behavior: it indicates that the hole should<br>be replaced only if a unique solution exists.<br><br>The list of the ten (at most) first solutions encountered can be<br>
included by using flag -l.<br><br>A particular solution can be selected by writing -s &lt;n&gt;, ... <br><br>===================<br><br>        On Wed, Nov 6, 2013 at 5:18 PM, Wolfram Kahl<br>             &lt;<a href="mailto:kahl@cas.mcmaster.ca">kahl@cas.mcmaster.ca</a> &lt;mailto:<a href="mailto:kahl@cas.mcmaster.ca">kahl@cas.mcmaster.ca</a>&gt;&gt;<br>
             wrote: The dot is warning you that the following<br>             identifier is currently not in scope --- you need to<br>             change the code to bring it into scope. Here, add:<br><br>             open import Data.Product using (proj₁)<br>
<br>        open import Data.Product using (proj₁) is there... <br><br>    The name .proj₁ does not refer to Data.Product.proj₁. I think it<br>    refers to the underscore in &quot;just (s , _ , p₁)&quot;.<br><br>Yes. I think it is a little bug, or a strange behaviour.<br>
<br></div><div class="gmail_quote">I replaced the case-of by:<br><br> case mgu2 (Var v) (Con c) of λ<br>   { nothing → nothing ; <br>     (just (s , p , p₁)) → just (s , comm_unif2&#39; p , {!!}) <br>   }<br> <br></div><div class="gmail_quote">
Thanks, cheers,<br><br>Carlos<br><br></div><br></div></div>