[Agda] Agda bug

[Wolfram Kahl]

Carlos,

On Wed, Nov 06, 2013 at 03:14:57PM -0200, Carlos Camarao wrote:
> When the cursor is placed inside { }₀, and Cntrl-c Cntrl-a is typed
> (meaning 'try to automatically fill the hole yourself if you can'),
> the compiler inserts "nothing" in the place of { }₀.
> 
> That is a bug (I think).
> 
> Furthermore, if I delete the inserted "nothing" and insert "just ?"
> the program is accepted by the compiler. The compiler replaces "?" by "{
> }₀":
> an inconsistency, since "nothing" was considered before the
> only possibility ("just ?" should thus not be accepted).

"nothing" was considered not as the ``only possibility'',
but as the ``first possibility that worked''.

To see all possibilities that are considered to work,
insert ``-l'' into the whole before hitting C-c C-a.


> /home/camarao/agda/bugs/bug5/Unif.agda:96,44-50
> .proj₁ is not a valid expression.
> when scope checking .proj₁
> 
> That is another bug (I think) (if it does not compile, it should have
> not been inserted). I am using compiler 2.3.0.1.

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₁)



Hope this helps!


Wolfram