Re: [OFFTOPIC] Re: Invoking a function from a list of functions

[Amin Bandali]

Stefan Monnier writes:

> FWIW, in the Agda language, it's very common to use non-ASCII characters
> which are input (in agda-mode) via a variant of the TeX input method.
> The reason this is tolerated is because those chars are already familiar
> to most users because they're used on paper for the same purpose.

Same with Lean: lean-mode comes with lean-input which is based on
agda-input with minor changes, and it makes it /super/ convenient
to insert commonly used unicode characters: \a for α, \b for β,
a\1 for a₁, \and for ∧, \|- for ⊢, and hundreds more.  I’ve
actually come to like lean-input so much that I’ve set it as my
default-input-method so I can toggle it with C-\ and easily type
unicode symbols whenever and wherever I want.

I’ve been experimenting with using lean-input along with the
unicode-math package (for {Lua,Xe}TeX) and it has drastically
improved my experience with writing and reading Org and TeX
documents.  It’s possible to change the input prefix from
backslash to something else to avoid clashes when writing TeX¹.

Footnotes:
¹  
https://git.sr.ht/~bandali/dotfiles/commit/e44b9b7eb100a3d5c1640b7df7d4c458f81998ab