<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"><<a href="mailto:carlos.camarao@gmail.com" target="_blank">carlos.camarao@gmail.com</a>></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 <<a href="mailto:kahl@cas.mcmaster.ca" target="_blank">kahl@cas.mcmaster.ca</a>> 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> > (meaning 'try to automatically fill the hole yourself if you can'),<br> > the compiler inserts "nothing" in the place of { }₀.<br>
><br> > That is a bug (I think).<br> ><br> > Furthermore, if I delete the inserted "nothing" and insert "just ?"<br> > the program is accepted by the compiler. The compiler replaces "?" by "{<br>
> }₀":<br> > an inconsistency, since "nothing" was considered before the<br> > only possibility ("just ?" should thus not be accepted).<br> <br> "nothing" was considered not as the ``only possibility'',<br>
but as the ``first possibility that worked''.<br><br> To see all possibilities that are considered to work,<br> insert ``-l'' into the whole before hitting C-c C-a.<br><br></div>Ok. Thanks.<br><br>
I'd expect (and suggest) a different behavior: that by default (that<br>
is, if nothing, i.e. no "-l", 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'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.</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'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'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>