coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lean Theorem Prover

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Lean Theorem Prover
Date: Mon, 7 Mar 2016 15:53:14 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:YoU42hDc3dPDtE8g+Rt8UyQJP3N1i/DPJgcQr6AfoPdwSP7/oMbcNUDSrc9gkEXOFd2CrakU1KyG6uu5Aj1IyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niKbiotaKOFQArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JeWGXlxdOHz/97Q2/G7z1uzb2u+41jCKeMMj7S6xyQTW+x6huQR7sziwAMmhqoynslsVsgfcD81qarBtlztuMbQ==

On 03/07/2016 01:33 PM, Saulo Araujo wrote:
> Maybe the popularization of fonts like
> https://github.com/i-tu/Hasklig and
> https://github.com/tonsky/FiraCode help in this matter. By the way,
> Visual Studio Code (an open source code centric IDE developed by
> Microsoft) has just added support to these fonts (more details in the
> section Ligatures for VS Code of
> https://code.visualstudio.com/Updates).

Note that this is a special case of prettification: instead of mapping
character sequences to common unicode characters, you map them to private
codepoints where an alternate representation of the corresponding character
is stored.

For example, instead of mapping ‘->’ to ‘→’, you map it to an alternate
character (0x110059 in the case of Fira Mono) which also looks like an arrow,
but has the right width.

Attachment: signature.asc
Description: OpenPGP digital signature

Re: [Coq-Club] Lean Theorem Prover, Emilio Jesús Gallego Arias, 03/07/2016
- Re: [Coq-Club] Lean Theorem Prover, Saulo Araujo, 03/07/2016
  - Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 03/07/2016