[Agda] Agda bug
Nils Anders Danielsson
nad at cse.gu.se
Thu Nov 7 17:30:45 CET 2013
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
> 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₁)".
More information about the Agda