<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 7, 2013 at 2:30 PM, Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>> 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's behavior:<br>
<br> "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. ..."<br><br> I had not read this, but even if I had, I could interpret "a solution"<br>
(in "The search carries on until either a solution..." above) as<br> "a unique solution": I think this is what auto should do unless<br> otherwise explicitly indicated. <br><br> I've modified the text on the wiki:<br>
<br> "The search carries on until either a (not necessarily unique)<br> solution is found, ..."<br><br> If Agda'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'd suggest to include a -u "parameter", 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 <n>, ... <br><br>===================<br><br> On Wed, Nov 6, 2013 at 5:18 PM, Wolfram Kahl<br> <<a href="mailto:kahl@cas.mcmaster.ca">kahl@cas.mcmaster.ca</a> <mailto:<a href="mailto:kahl@cas.mcmaster.ca">kahl@cas.mcmaster.ca</a>>><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 "just (s , _ , p₁)".<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' p , {!!}) <br> }<br> <br></div><div class="gmail_quote">
Thanks, cheers,<br><br>Carlos<br><br></div><br></div></div>