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

[Rusi]

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(?) 
etc?