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: Thu, 25 Feb 2016 10:47:50 -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:m4x4dBSoq3WKQyT2OVM5aaQqNdpsv+yvbD5Q0YIujvd0So/mwa64YBGN2/xhgRfzUJnB7Loc0qyN4/+mBzVLvc3JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuNOk4U33KUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzA9lptNDg7Z2yn7QtK0mS/zq+Zw3GHONsn7SL0yRXK67rtDRxrhiSNBPDk8pjKEwvdshb5W9Ury7yd0xJTZNdmY

On 02/25/2016 10:29 AM, roux cody wrote:
> and auto-completes in the eclipse style
We're working on this :)

Is there anything in lean-mode that is not described in
https://leanprover.github.io/presentations/20150123_lean-mode/lean-mode.pdf ?
Most of what's in there seems to already be available for Coq.

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Lean Theorem Prover, Saulo Araujo, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Jonathan Leivent, 02/25/2016
  - RE: [Coq-Club] Lean Theorem Prover, Soegtrop, Michael, 02/25/2016
    - Re: [Coq-Club] Lean Theorem Prover, Benjamin Pierce, 02/25/2016
      - RE: [Coq-Club] Lean Theorem Prover, Soegtrop, Michael, 02/25/2016
  - Re: [Coq-Club] Lean Theorem Prover, Freek Wiedijk, 02/25/2016
    - Re: [Coq-Club] Lean Theorem Prover, Théo Zimmermann, 02/25/2016
    - Re: [Coq-Club] Lean Theorem Prover, Bas Spitters, 02/25/2016
      - Re: [Coq-Club] Lean Theorem Prover, roux cody, 02/25/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/25/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/25/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Jonathan Leivent, 02/25/2016
    - Re: [Coq-Club] Lean Theorem Prover, John Wiegley, 02/25/2016
- 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