[Agda] Lambda

[Nils Anders Danielsson]

On Wed, Jun 18, 2008 at 6:43 PM, Anton Setzer <A.G.Setzer at swansea.ac.uk> wrote:
>
> There is an easy way of using such symbols (and other
> special symbols) by using the abbreviation mode.

Yes, I have documented this as one possible way forward:

  http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Docs.UnicodeInput
  (Last section.)

However, I would not say that it is easy. Someone has to compile a
table of "abbreviations", and this can involve quite a lot of work,
especially if we want to have a good, consistent naming convention.

So, do we really want to construct and maintain a special input method
for Agda, instead of using out-of-the-box solutions? The
out-of-the-box solutions are not optimal, but designing our own one
requires work, and increases fragmentation on the input method scene.

On balance I think that it could be a good idea to design our own
method, but someone needs to do the work. One approach is for someone
to come up with a good (tested) naming convention, and then we can
expand the initial "abbreviation" tables collaboratively, perhaps
through the Agda wiki.

Another option is to improve the standard Emacs input methods, but
given the slow release cycle of Emacs this seems like a bad idea. Does
anyone know if there are any non-Emacs-specific input methods which
handle Unicode symbols? (Not counting the methods of clicking in a
character table or entering code points manually.)

> By the way, a list of symbols usable in leim
> can be found here:
>
> http://www.cs.swan.ac.uk/~csetzer/othersoftware/agda2/leimListOfSymbols.txt

Note that we cannot simply steal this list (and then modify it
according to our circumstances); LEIM is GPL-ed, so we would get
licensing issues.

-- 
/NAD