[Agda] Agda bug

[Nils Anders Danielsson]

On 2013-11-07 13:43, Carlos Camarao wrote:
> The documentation (from
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Auto) is not
> very clear about auto's behavior:
>
> "Search parameters are given by entering them into the hole before
> invocation. Giving no arguments is fine and results in a search with
> default parameters. The search carries on until either a solution is
> found, the search space is fully (and unsuccessfully) explored or it
> times out (5 seconds by default). Here follows a list of the different
> modes and parameters. ..."
>
> I had not read this, but even if I had, I could interpret "a solution"
> (in "The search carries on until either a solution..." above) as
> "a unique solution": I think this is what auto should do unless
> otherwise explicitly indicated.

I've modified the text on the wiki:

   "The search carries on until either a (not necessarily unique)
   solution is found, ..."

If Agda's unifier instantiates a meta-variable with a non-unique
solution, then this is a bug. However, C-c C-a is allowed to find
non-unique solutions.

> On Wed, Nov 6, 2013 at 5:18 PM, Wolfram Kahl <kahl at cas.mcmaster.ca <mailto:kahl at cas.mcmaster.ca>> wrote:
>      The dot is warning you that the following identifier is currently not in scope ---
>      you need to change the code to bring it into scope. Here, add:
>
>      open import Data.Product using (proj₁)
>
> open import Data.Product using (proj₁) is there...

The name .proj₁ does not refer to Data.Product.proj₁. I think it refers
to the underscore in "just (s , _ , p₁)".

-- 
/NAD