<div dir="ltr"><br><div class="gmail_extra"><div class="gmail_quote">On Thu, Nov 7, 2013 at 1:43 PM, Carlos Camarao <span dir="ltr">&lt;<a href="mailto:carlos.camarao@gmail.com" target="_blank">carlos.camarao@gmail.com</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="im">On Wed, Nov 6, 2013 at 5:18 PM, Wolfram Kahl &lt;<a href="mailto:kahl@cas.mcmaster.ca" target="_blank">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></div>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" target="_blank">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.</div></blockquote><div><br></div>

<div>There are a few problems with this approach:</div><div>- It would mean auto could only be used in cases where the search space</div><div>  can be exhaustively explored in a short time. You wouldn&#39;t want auto to</div>

<div>  spend a lot of time just to make sure that the solution it found right away</div><div>  is the unique one.</div><div>- Often you don&#39;t care about having a unique solution. For example, if you</div><div>  want it to prove some simple lemma any proof would do.</div>

<div><br></div><div>/ Ulf</div><div><br></div></div></div></div>