[Agda] Emacs interface

[Nils Anders Danielsson]

On 2009-04-08 09:35, Andreas Abel wrote:
> 
> Like the
> 
>   %name <TyFam> <NamePrefix>.
> 
> pragma in Twelf?
> 
> You can give each inductive family <TyFam> a default <NamePrefix> for 
> system-generated names.

That is even more limited than the current scheme. I like to use
definitions like the following one:

  data Ty : Set where
    _⟶_ : (σ τ : Ty) → Ty

If name suggestion works on a per-type basis then you cannot have
different names (name prefixes) for different arguments.

The two methods could be combined, though.

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