Comment by nemo1618 1 year ago my hot take: the language should accept \, but formatters should replace it with λ 1 comment nemo1618 Reply IshKebab 1 year ago Lean does symbols very well. You can just type \r and it will replace it with a right arrow as you type.
IshKebab 1 year ago Lean does symbols very well. You can just type \r and it will replace it with a right arrow as you type.
Lean does symbols very well. You can just type \r and it will replace it with a right arrow as you type.