The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 8 Mar 2013 15:23:31 -0500,
"Benjamin C. Pierce" 
<bcpierce AT cis.upenn.edu>
 a écrit :

> Thanks, Cédric (and Arthur, who wrote offline with similar
> suggestions)!
> 
> I do want to stay with ascii, to avoid forcing too many people to
> struggle with how to edit unicode.  But the other solutions do seem
> pretty reasonable -- my current favorite is [{P} c {Q}].  Another
> option we're considering is to keep {{P}}c{{q}} but fix up the HTML
> output so that the braces come out close together.  

Note that you can also have two syntaxes, a unicode one and an ascii
one. That is people can input ascii notations and see unicode notation
when calling the printer (ascii for input and unicode for output).

For instance, if you "Require Import Utf8.",

Definition id := fun {A : Type} (a : A) => a.

Print id.

will return "id = λ {A:Type} (a:A), a"

The not so good thing, is that if you aim at persons who have no
support for unicode (such as someone using coqtop on a tty, if that
exists), you should put all unicode notations on a separate .v file
which is to be required for people which fully support unicode (and
want some nice pretty printing).

> 
> I'm still hoping someone will tell me that it's possible to make
> {P}c{Q} work… :-)
> 
>     - B