[Agda] Lambda

[Marcin Benke]

2008/6/18 Nils Anders Danielsson <nils.anders.danielsson at gmail.com>:
>
> By the way, do you mean that we should allow both the old ASCII names
> and the nicer-looking characters?
>
> Pros: Agda can still be used with only ASCII characters; you can try
> out the language without knowing how to input "non-standard"
> characters. (But you cannot use the standard library...)
>
> Cons: More reserved words.

I would be strongly in favour of keeping the ASCII version, first for
the reason Nisse mentioned, and second for backwards compatibility
(which is of course not a holy cow, but still not without importance).
Maybe we can consider dropping ASCII for Agda3 when the time comes
though :)
-- 
Marcin Benke