[Agda] Emacs interface

[Andreas Abel]

On Apr 7, 2009, at 5:42 PM, Nils Anders Danielsson wrote:

> 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.

Like the

   %name <TyFam> <NamePrefix>.

pragma in Twelf?

You can give each inductive family <TyFam> a default <NamePrefix> for  
system-generated names.

Maybe this can be extended to type skeletons, such that one can

   %name (el _ -> U) f

for instance.

That does not solve the problem for polymorphism, though, it does not  
tell the system how to generate a name for

   ? : A,  where A : Set is a local assumption

Cheers,
Andreas