From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED!not-for-mail From: Rusi Newsgroups: gmane.emacs.help Subject: Re: [OFFTOPIC] Re: Invoking a function from a list of functions Date: Wed, 28 Nov 2018 06:14:38 -0800 (PST) Message-ID: References: <67c4a534-d41c-4736-8839-c2dbbdf7f9c2@googlegroups.com> <2da7504a-8bbf-41b9-993e-a7bacd6c97b2@googlegroups.com> <20181116114002.3ba6bcc8dc1e699ba58e08b8@speakeasy.net> <20181119172358.802ce30c54f2fd20f8c300c4@speakeasy.net> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Trace: blaine.gmane.org 1543414427 13134 195.159.176.226 (28 Nov 2018 14:13:47 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Wed, 28 Nov 2018 14:13:47 +0000 (UTC) Injection-Date: Wed, 28 Nov 2018 14:14:38 +0000 User-Agent: G2/1.0 To: help-gnu-emacs@gnu.org Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Wed Nov 28 15:13:43 2018 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gS0az-0003G6-TN for geh-help-gnu-emacs@m.gmane.org; Wed, 28 Nov 2018 15:13:42 +0100 Original-Received: from localhost ([::1]:48004 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gS0d6-00027o-4y for geh-help-gnu-emacs@m.gmane.org; Wed, 28 Nov 2018 09:15:52 -0500 X-Received: by 2002:a37:b147:: with SMTP id a68mr3779403qkf.0.1543414478721; Wed, 28 Nov 2018 06:14:38 -0800 (PST) X-Received: by 2002:aed:3863:: with SMTP id j90mr64118qte.0.1543414478571; Wed, 28 Nov 2018 06:14:38 -0800 (PST) Original-Path: usenet.stanford.edu!v55no1530761qtk.0!news-out.google.com!h3ni727qtk.1!nntp.google.com!v55no1530754qtk.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Original-Newsgroups: gnu.emacs.help In-Reply-To: Complaints-To: groups-abuse@google.com Original-Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=103.207.182.185; posting-account=mBpa7woAAAAGLEWUUKpmbxm-Quu5D8ui Original-NNTP-Posting-Host: 103.207.182.185 Original-Xref: usenet.stanford.edu gnu.emacs.help:224663 X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.21 Precedence: list List-Id: Users list for the GNU Emacs text editor List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Original-Sender: "help-gnu-emacs" Xref: news.gmane.org gmane.emacs.help:118791 Archived-At: On Tuesday, November 20, 2018 at 11:45:44 AM UTC+5:30, Amin Bandali wrote: > Stefan Monnier writes: >=20 > > FWIW, in the Agda language, it's very common to use non-ASCII character= s > > 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 familia= r > > to most users because they're used on paper for the same purpose. >=20 > 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 =CE=B1, \b for =CE=B2, > a\1 for a=E2=82=81, \and for =E2=88=A7, \|- for =E2=8A=A2, and hundreds m= ore. I=E2=80=99ve > actually come to like lean-input so much that I=E2=80=99ve 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=E2=88=83=E2=88=80N !] Do you have a good comparison of the contenders lean, agda, idris isabelle(= ?) etc?