coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lean Theorem Prover

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Lean Theorem Prover
Date: Fri, 26 Feb 2016 09:20:04 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:U/lbXBIt50IUOsQ889mcpTZWNBhigK39O0sv0rFitYgULvnxwZ3uMQTl6Ol3ixeRBMOAu60C1bGd7vyocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0ILpjKvvp9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF6k4voZX2MKpSJJH02AxxXzQ5v8tmOuve5w3SScIYvuTKwcVjGr7qMtQxjt3nRUfwUl+X3a35QjxJlQpwis8kRy

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.

Attachment: signature.asc
Description: OpenPGP digital signature

Re: [Coq-Club] Lean Theorem Prover, (continued)
- Re: [Coq-Club] Lean Theorem Prover, Daniel Schepler, 02/25/2016
  - Re: [Coq-Club] Lean Theorem Prover, Abhishek Anand, 02/25/2016
    - Re: [Coq-Club] Lean Theorem Prover, Daniel Schepler, 02/26/2016
      - Re: [Coq-Club] Lean Theorem Prover, roux cody, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Jonathan Leivent, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Arnaud Spiwack, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Benjamin C. Pierce, 02/26/2016
        RE: [Coq-Club] Lean Theorem Prover, Soegtrop, Michael, 02/26/2016
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/26/2016
        
        RE: [Coq-Club] Lean Theorem Prover, Makarius, 02/26/2016
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/26/2016
        Re: [Coq-Club] Lean Theorem Prover, Makarius, 02/26/2016
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/27/2016
        Re: [Coq-Club] Lean Theorem Prover, Makarius, 02/27/2016
        Re: [Coq-Club] Lean Theorem Prover, Enrico Tassi, 02/27/2016