[Agda] Re: Lambda
Nils Anders Danielsson
nad at Cs.Nott.AC.UK
Sat Nov 15 00:01:53 CET 2008
On 2008-11-14 20:58, Stefan Monnier wrote:
>> 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.
>
> Another option of course is to ask Emacs to display \ as λ and -> as →.
Assuming that the actual λ and → really meant the same as \ and ->,
because otherwise it would be confusing.
(This is orthogonal to the issue about how to input various symbols, by
the way. Agda now has a dedicated input method, see
http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Docs.UnicodeInput.)
--
/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.
More information about the Agda
mailing list