[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: Amin Bandali
Subject: Re: [OFFTOPIC] Re: Invoking a function from a list of functions
Date: Tue, 20 Nov 2018 01:15:31 -0500
User-agent: Gnus/5.13 (Gnus v5.13) Emacs/27.0.50 (gnu/linux)

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


reply via email to

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