<div dir="ltr">On Wed, Nov 6, 2013 at 5:18 PM, Wolfram Kahl <<a href="mailto:kahl@cas.mcmaster.ca">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>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">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> > /home/camarao/agda/bugs/bug5/Unif.agda:96,44-50<br>
> .proj₁ is not a valid expression.<br> > when scope checking .proj₁<br> ><br> > That is another bug (I think) (if it does not compile, it should have<br> > 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>