coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lean Theorem Prover

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Lean Theorem Prover
Date: Sat, 27 Feb 2016 17:54:28 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:A7g8kh/+vpmJ0f9uRHKM819IXTAuvvDOBiVQ1KB90O0cTK2v8tzYMVDF4r011RmSDdqdta8P2rCempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lRciM0o/mjaibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEzuSxGO7XxUbmwNiRsAVwXD9hDxWdHtuzDht8J83jObNIv4V+ZnCnyZ8653RUqw2288PDkj/TSPhw==

On Sat, Feb 27, 2016 at 05:25:26PM +0100, Makarius wrote:
> This is again in conflict with "minimize assumptions about available
> technology".
>
> I recall the Matita guys trying to provide smarter text boxes for OCaml GTK
> (based on MathML). Did this ever reach the big masses of users on all
> platforms?

Sadly no. Also GTK+ cannot really be considered cross platform :-/
Recent version of Matita output plain utf8 text.

Ciao
--
Enrico Tassi

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