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

[Stefan Monnier <monnier@iro.umontreal.ca>]

> 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.

Maybe we should add a "math" input method along the lines of those
Agda/Lean input methods.  I currently use the TeX input method for such
purposes but it tends to be a bit more verbose than I like.

> It’s possible to change the input prefix from
> backslash to something else to avoid clashes when writing TeX¹.

In my experience (using the TeX input method when writing LaTeX),
I think the main problem with the clash on \ is that when the LaTeX
command I write has a valid prefix in the input method, the input method
rewrites that prefix.  If we could fix it so that "\b" inputs "β" but
"\beta" isn't rewritten to "βeta" then I might even be able to have \
play both roles without going bonkers.


        Stefan