coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lean Theorem Prover

From: Saulo Araujo <saulo2 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Lean Theorem Prover
Date: Fri, 26 Feb 2016 21:05:07 -0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=saulo2 AT gmail.com; spf=Pass smtp.mailfrom=saulo2 AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f45.google.com
Ironport-phdr: 9a23:TDvw9RNHW8P0j4u4aQEl6mtUPXoX/o7sNwtQ0KIMzox0KP/5rarrMEGX3/hxlliBBdydsKIbzbSK+Pm5EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35vxibz5osSbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSJDUgKWE8osPx5jfZSg7a3XIBVmJeuwBBHgrCpEXhV4r1tXHSue902S3cNsrzG+NnEQ++5rtmHUe7wBwMMCQ0pTna

Oops, an important character was missing in the previous email: What I meant was "but that's ok :)"

Saulo

On Fri, Feb 26, 2016 at 8:52 PM, Saulo Araujo <saulo2 AT gmail.com> wrote:

Hi,

I´d like to thank everybody who took some time to share his impressions about Lean. The thread has changed a little bit and now we are talking about Unicode, but that's ok :

Saulo

On Fri, Feb 26, 2016 at 7:58 PM, Daniel Schepler <dschepler AT gmail.com> wrote:
On Fri, Feb 26, 2016 at 6:34 AM, Benjamin C. Pierce
<bcpierce AT cis.upenn.edu> wrote:
> (more significantly) I wonder whether the world has stabilized to the point
> where the major Coq IDEs will “just work” with unicode in their default
> configurations on all platforms.

As just one data point - on Debian GNU/Linux, the GTK-based CoqIDE
just works with unicode. As for inputting unicode characters, it took
a bit more effort - but the instructions at
https://coq.inria.fr/cocorico/TeXInputMethodForUnicodeNotations under
"In CoqIDE (using UIM on POSIX systems)" were all I needed to get that
working.
--
Daniel

Re: [Coq-Club] Lean Theorem Prover, (continued)