lambda / lamda

Stream: general

[Alistair Tucker]

Is there maybe some special unicode character I can use for a variable name? I thought maybe \lamda was it but it seems to do just the same as \lambda

[Floris van Doorn]

There are a few greek letters that cannot be used in declaration names or variable names, due to there use in type theory (at least in Lean 3). I think this only concerns λ, Π and Σ

[Alistair Tucker]

Yes thanks but I wondered if there was some unicode variation that I could use

[Alex J. Best]

I don't see any variants searching through https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json, other than upper case lambda

[Julian Berman]

There's «λ» if that counts.

[Kevin Buzzard]

Because of this issue Lean 4 uses fun, but you can use lambda for functions anyway in lean 4, so I conjecture that using lambda for e.g. real scalars (which is common in mathematics) might still not be possible even in Lean 4.