[Agda] Emacs interface

[Darin Morrison]

On Sun, Apr 5, 2009 at 7:03 PM, Wouter Swierstra <wouter at chalmers.se> wrote:

> First of all, I seem to be able to construct terms by iteratively refining
> goals that, when I reload the file, don't type check. I don't have an
> example at hand. Is this a known issue?

I've run into this issue several times too.

> A more minor issue: there are sometimes some spurious spaces left lying
> about after refining a goal. It'd be nice if this could be avoided.

Does this still happen for you with the most recent version of the
emacs mode?  I used to see this in older versions but I think it may
be fixed now (at least I don't notice it anymore).

> It would also be nice to customise the name generation when case splitting.
> I tend to avoid using C-c C-c because the generated names are really
> horrible. Should there be a pragma for this?

You may already be aware of it, but you can customize the names by
naming the constructors in the inductive definition:

data List (α : Set) : Set where
  []  : List α
  _∷_ : (x : α) (xs : List α) → List α

If you then case split on a variable of type List α, it will use (x ∷
xs) for the cons case.

I find this generally works pretty well.  The obvious downside is that
it can make the inductive definitions a little bit harder to read.

-- 
Darin