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 20:52:42 -0300
Authentication-results: mail2-smtp-roc.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-f50.google.com
Ironport-phdr: 9a23:esd09xYJcSYGmdim/bdCzJr/LSx+4OfEezUN459isYplN5qZpc+4bnLW6fgltlLVR4KTs6sC0LqJ9f68EjVZqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7/0pcGYOlwArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JaWwLlh0AKhLM8RP9FsPquzb+sbBV1yyTPMmwRrcxD2fxp5x3QQPl3X9UfwUy93va35R9

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)