[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: Rusi
Subject: Re: [OFFTOPIC] Re: Invoking a function from a list of functions
Date: Wed, 28 Nov 2018 06:14:38 -0800 (PST)
User-agent: G2/1.0

On Tuesday, November 20, 2018 at 11:45:44 AM UTC+5:30, Amin Bandali wrote:
> 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.

Thanks for pointing out lean to me
[And not just because its spelt L∃∀N !]

Do you have a good comparison of the contenders lean, agda, idris isabelle(?) 

reply via email to

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