The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

Since we’re talking about unicode, I’d like to get people’s advice…  

At some point, I’d really like to convert Software Foundations to unicode, as this would avoid a lot of hassles with notation, awkward hacks in HTML generation, etc.  But I’ve been nervous about making the switch so far for two reasons:

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

What do people think?  Should I just take the plunge?  Or is it not time yet?

    - Benjamin

On Feb 26, 2016, at 9:20 AM, Clément Pit--Claudel <clement.pit AT gmail.com> wrote:

On 02/26/2016 01:23 AM, Arnaud Spiwack wrote:

I just mean I like the agda-style input which replaces \forall by the unicode ∀ seamlessly. It's possible that this is supported in coq as well I guess (I'm a little behind the times).

That's just built-in in emacs. There are even several ways to do that (the old-school quail, and the newish company-math at least).

Indeed; with plain Emacs, just typing `M-x set-input-method RET TeX RET` will give you the Agda-style input that you mentionned.
Alternatively (if you use it), company-coq loads company-math, so typing \rightarr will offer \rightarrow, and RET will complete it to →.

Should we make this the default input method in PG?

Clément.