The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

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).

Best regards,

Saulo

On Mon, Mar 7, 2016 at 3:06 PM, Emilio Jesús Gallego Arias <e+coq-club AT x80.org> wrote:

I arrive pretty late to the thread but I'd like to add our two cents:

"Benjamin C. Pierce" <bcpierce AT cis.upenn.edu> writes:

> I wonder whether beginning users will find the available input methods
> confusing or off-putting, and (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.

Regarding these questions, in jsCoq (and thus in courses using it)
we've made the following choices:

+ Assume Coq users know LaTeX: unicode input is done by typing latex
  commands, as in emacs.

  Whether this is off putting to students, we don't know, but we assume
  to know a bit of TeX cannot harm too much.

  [Adding a toolbar with symbols would be pretty easy]

+ No pretty-fication: thus no confusion between \leq and ≤ .

+ We believe Unicode should work seamlessly in all supported platforms
  (thanks to webfonts).

We'd be very interested to hear whether some use cases are not covered
by these constrains.

Best regards,
Emilio