The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

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