coq-club AT inria.fr
Subject: The Coq mailing list
List archive
RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)
Chronological Thread
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)
- Date: Wed, 2 Mar 2016 09:03:11 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga03.intel.com
- Ironport-phdr: 9a23:5OBMYhRyYbw1X8lIMTN39M2GZ9psv+yvbD5Q0YIujvd0So/mwa64YxeN2/xhgRfzUJnB7Loc0qyN4/+mBjVLuMze+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8KVPFwD3WDiKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESukSBzM/dmsx+cfDtB/ZTALJ6GFWGjEdlQMNCAzY5jn7WI3wu230rLwu9jOdOJi8drc5Vii46L8vADrpgycOOjpzuDXSi8dwha9f5gmmqhNj2YnMSICTKPd6OKjaeIVJFiJ6Qs9NWnkZUcuHZIwVAr9ZMA==
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
- [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/01/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/01/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Enrico Tassi, 03/01/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Pierre-Marie Pédrot, 03/01/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/01/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Matej Kosik, 03/01/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/01/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Vincent Laporte, 03/01/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/01/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/02/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Pierre-Marie Pédrot, 03/02/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Ralf Jung, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Enrico Tassi, 03/02/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Pierre-Marie Pédrot, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Gabriel Scherer, 03/03/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Enrico Tassi, 03/03/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/01/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Matej Kosik, 03/01/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/01/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Pierre-Marie Pédrot, 03/01/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Enrico Tassi, 03/01/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/01/2016
Archive powered by MHonArc 2.6.18.