coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] 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] Lean Theorem Prover
Date: Thu, 25 Feb 2016 08:37: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 mga01.intel.com
Ironport-phdr: 9a23:B+WWOBWlCuy+eSdUxeN7HrFa7DTV8LGtZVwlr6E/grcLSJyIuqrYZhOEt8tkgFKBZ4jH8fUM07OQ6PC/HzFRqs/Z7zgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oM2MJVgZz2PlPvtbF1afk0b4joEum4xsK6I8mFPig0BjXKBo/15uPk+ZhB3m5829r9ZJ+iVUvO89pYYbCf2pN/dwcbsNRj8hKiU+4NDhnRjFVwqGoHUGGC1CmR1RRgPB8RvSX5HrsyK8uPAriweAOsijB4szVDu+9aBzDFfNiSwHPjM9uimDj817jKtWpFS6oBFw35TTeKmUMuZzeuXWetZMFjkJZdpYSyEUWtD0VIAIFedUZes=

Dear Saulo,

since they are looking into automation, I wonder if they plan to use Z3 for
some of its backend work. The manual doesn't mention Z3 ...

Otherwise the choice between Lean and Coq looks like the choice between F#
and OCaml.

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] 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