[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Stefan Monnier
Subject: Re: [OFFTOPIC] Re: Invoking a function from a list of functions
Date: Wed, 21 Nov 2018 10:05:25 -0500
User-agent: Gnus/5.13 (Gnus v5.13) Emacs/27.0.50 (gnu/linux)

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


reply via email to

[Prev in Thread] Current Thread [Next in Thread]