[Agda] Emacs interface

[Nils Anders Danielsson]

On 2009-04-06 01:06, Darin Morrison wrote:

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

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

I almost always give default names to all constructor arguments, because
otherwise case-split is not very useful. This is far from perfect,
though. For instance, when writing about Agda code I want to avoid such
clutter, so I often remove all the inessential names. A better solution
to this problem would be welcome.

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.