coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lean Theorem Prover

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Lean Theorem Prover
Date: Thu, 25 Feb 2016 11:22:57 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f41.google.com
Ironport-phdr: 9a23:VRlszRDHytztOsP4byx+UyQJP3N1i/DPJgcQr6AfoPdwSP74rsbcNUDSrc9gkEXOFd2CrakU1KyI6uu8AiQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTokb7rsMGIKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs1kbVGwKkhNOSyzI7Q/3WIu55in9sOt+1S2XMOX5SLk1XXKp6KI9G0ygszsOKzNsqDKfscd3lq8O+B8=

Is there a way in Lean for users to define new tactics, as with Ltac?

Is there any extraction capability?

As for building-in proof irrelevance (while having a separate HoTT mode) that might not bother anyone but me: I (ab)use proof *relevance* in Coq as a way to get really good erasability.

-- Jonathan

Re: [Coq-Club] Lean Theorem Prover, (continued)
- 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
        
        Re: [Coq-Club] Lean Theorem Prover, Benjamin C. Pierce, 02/26/2016
        RE: [Coq-Club] Lean Theorem Prover, Soegtrop, Michael, 02/26/2016