The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Team & Users,

> Here is a software that provides a “compose key” for MS-Windows:
> 
> https://github.com/samhocevar/wincompose

I had a look at WinCompose as Math IME as suggested by Vincent Laporte (test 
machine is Win7 64). It works well with CoqIDE and any other SW I tested and 
it reuses the Linux Xcompose file. The license of wincompose as well as of 
the used Xcompose file is a permissive open source license. It doesn't 
require complicated installation (just unzip and run the exe).

So how about bundling this with CoqIDE for Windows and using Xcompose on 
Linux (and I guess also Mac).
One change I would do in Wincompose is that it checks if it is already 
started and exits immediately if so. Then CoqIDE could just spawn WinCompose 
to make sure it is loaded.

Some important sequences are as follows:

Compose A A for "forall"
Compose E E for "exists"
Compose - > for "arrow right"
Compose < - for "arrow left"
Compose <-> for "arrow double

The Compose key (by default right alt) is pressed and released - not hold.
For forall the A is upper case, so it has to be pressed with shift.
One little down side is that some sequences have a common header like <- and 
<->. So the <- symbol appears only after one presses a character which 
doesn't lead to known sequence, like space.
Not sure if it would be more convenient to require that the Compose key is 
kept held down to avoid this.

Of cause it would be possible to add additional sequences like 

Compose forall   for "forall"
Compose exists for "exists"
Compose implies for "arrow right"

The following abbreviations are also still free:

Compose fa  for "forall"
Compose ex for exists
Compose imp for implies

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928