[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