[Agda] Lambda

[Nils Anders Danielsson]

On Wed, Jun 18, 2008 at 6:42 AM, Lennart Augustsson
<lennart at augustsson.net> wrote:
>
> I'd like a nice looking lambda in Agda.  How about allowing U+22CB
> as lambda?

In case anyone wonders: U+22CB is LEFT SEMIDIRECT PRODUCT (⋋;
\leftthreetimes with the TeX input method).

Did you choose not to suggest U+03BB GREEK SMALL LETTER LAMDA (λ;
\lambda) because you want to allow Greek people (and others) to use
the ordinary lambda in identifiers? By letting the lambda character be
a keyword instead of a reserved character (i.e. forcing people to
insert a space between the lambda and the first bound variable) this
would not be much of an issue.

(Currently \ is something of a hack. There is no need to insert a
space if the following character is alphabetic, but otherwise space is
necessary.)

> Likewise, I'd like something nicer than -> for the function arrow, how
> about U+2192?

U+2192 is RIGHTWARDS ARROW (→; \to).

And a nicer variant of forall would be U+2200 FOR ALL (∀; \forall)

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.

-- 
/NAD