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)

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: Tue, 1 Mar 2016 12:23:06 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.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 mga14.intel.com
Ironport-phdr: 9a23:3OG1wB3ic0Y0xUT3smDT+DRfVm0co7zxezQtwd8ZsegRK/ad9pjvdHbS+e9qxAeQG96LtLQb06GN7ejJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6NyZvvnLvss7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JsKWqLjOq88ULZwDTI8Mmlz6teh/U3IShLK7X8BWE0XlABJCk7L9kepcI32t36wje1w1zWAOtWyBZU1UjSr4qMhAEvtiSwHPjM9tnrQh8NslqVDiBOnuxF7hYXTZdfGZ7JFYqrBcIZCFiJ6VcFLWnkZDw==

Dear Vincent,

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

An interesting feature of this is that it seems to use the same file format
as Xcompose for X.
The one thing I am not sure about is if one should use an IME (something that
is recognized by Windows as an IME) or some post processor like this. Since I
don't think IMEs can be stackes, I guess such a postprocessor is more
deseriable for those languages which require an IME.

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