[Agda] "Not in scope" error

[Antoine Durand-Gasselin]

On 02 Jul 2008 at 19:17, Robert Rothenberg <robrwo at gmail.com> wrote:

> On 02/07/08 19:06 Nils Anders Danielsson wrote:
>> On Wed, Jul 2, 2008 at 5:47 PM, Robert Rothenberg <robrwo at gmail.com> wrote:
>>> However, I still get the error
>>
>> Can you send a complete example exhibiting the problem?
>>
>
> open import Relation.Binary
> open import Data.Bool
> open import Data.List
>
> module Labels {a : Set} (_==_ : a -> a -> Bool) where
>
> data Transposition (a : Set) : Set where
>   ≪_,_≫ : a -> a -> Transposition a
>
> _·'_ : Transposition a -> a -> a
> ≪ x , y ≫ ·' z = if (z == x) then y
>                 else if (z == y) then x
>                 else z
>
> _·_ : {a : Set} -> [ Transposition a ] -> a -> a
> []        · z = z
> (t :: ts) · z = ts · (t ·' z)
>

This will not typecheck, for _==_ is parametrized by a. If you want your
functions to be polymorphic, you will need _==_ to be polymorphic.
You may want to define your module like that then:
module Labels (_==_ : {a : Set} -> a -> a -> Bool) where


I would use case-split like that (editing this file with emacs and agda
major mode loaded):

I first write:
_·_ : {a : Set} -> [ Transposition a ] -> a -> a
list · z = ?

Then reload agda, place my cursor in the goal and invoke
agda2-make-cases (with C-c C-c). Then emacs will prompt me the name of
variable I want to make-cases on.

Some pieces of code are really boring to write and the emacs mode
provides a nice help then. I have a problem however: I have the feeling
that the emacs mode regularily reloads the entire file, which is time
consumming on large files. For exemple everywhen I make-cases. Or when I
want to check a function definition, can't I *only* check that function
definition ?


-- 
Antoine DG