<div dir="ltr">On Wed, Nov 6, 2013 at 5:18 PM, Wolfram Kahl &lt;<a href="mailto:kahl@cas.mcmaster.ca">kahl@cas.mcmaster.ca</a>&gt; wrote:<br><br>    Carlos,<br><br>    On Wed, Nov 06, 2013 at 03:14:57PM -0200, Carlos Camarao wrote:<br>
      When the cursor is placed inside { }₀, and Cntrl-c Cntrl-a is typed<br>    &gt; (meaning &#39;try to automatically fill the hole yourself if you can&#39;),<br>    &gt; the compiler inserts &quot;nothing&quot; in the place of { }₀.<br>
    &gt;<br>    &gt; That is a bug (I think).<br>    &gt;<br>    &gt; Furthermore, if I delete the inserted &quot;nothing&quot; and insert &quot;just ?&quot;<br>    &gt; the program is accepted by the compiler. The compiler replaces &quot;?&quot; by &quot;{<br>
    &gt; }₀&quot;:<br>    &gt; an inconsistency, since &quot;nothing&quot; was considered before the<br>    &gt; only possibility (&quot;just ?&quot; should thus not be accepted).<br>    <br>    &quot;nothing&quot; was considered not as the ``only possibility&#39;&#39;,<br>
    but as the ``first possibility that worked&#39;&#39;.<br><br>    To see all possibilities that are considered to work,<br>    insert ``-l&#39;&#39; into the whole before hitting C-c C-a.<br><br>Ok. Thanks.<br><br>I&#39;d expect (and suggest) a different behavior: that by default (that<br>
is, if nothing, i.e. no &quot;-l&quot;, is inserted) auto would only fill a hole<br>if a unique solution was found; the behavior of inserting the first<br>found solution (or of showing all found solutions) should have to be<br>
explicitly indicated.<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>    &gt; /home/camarao/agda/bugs/bug5/Unif.agda:96,44-50<br>
    &gt; .proj₁ is not a valid expression.<br>    &gt; when scope checking .proj₁<br>    &gt;<br>    &gt; That is another bug (I think) (if it does not compile, it should have<br>    &gt; not been inserted). I am using compiler 2.3.0.1.<br>
    The dot is warning you that the following identifier is currently not in scope ---<br>    you need to 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>    Hope this helps!<br><br>    Wolfram <br><br>Thanks a lot. <br><br>Cheers,<br><br>Carlos<br><br><br></div>