[Agda] Lambda

[Nils Anders Danielsson]

On Thu, Jun 19, 2008 at 8:43 PM, Anton Setzer <A.G.Setzer at swansea.ac.uk> wrote:
>
> I have been using abbrev mode for a long time when editing latex documents,
> because the backslash key is so difficult to reach.

I have remapped the backslash key to a more prominent position on my
keyboard. :) But I don't expect every Agda user to do this.

> So in latex my convention is that the abbreviation consists of
> omitting the backslash and doubling the last character.

Note to others: In abbrev mode abbreviations are expanded when the
cursor is at the end of an abbreviation and you type a character which
is not a word constituent. You can also expand abbreviations outside
of abbrev mode, by typing some key combination.

I think that it would be a good idea to define a raw mapping of names
to characters (without any character doubling, for instance), but make
it possible for the user to customise the mapping using a function.
Then we can try out several different schemes, and provide some
defaults.

I would probably prefer using the raw names, and expand abbrevs using
a dedicated key, but with a flexible mechanism it should be possible
to satisfy both your and my tastes.

-- 
/NAD