coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lean Theorem Prover

From: Daniel Schepler <dschepler AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Lean Theorem Prover
Date: Thu, 25 Feb 2016 15:01:12 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dschepler AT gmail.com; spf=Pass smtp.mailfrom=dschepler AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f179.google.com
Ironport-phdr: 9a23:BYOdth/h7JInzP9uRHKM819IXTAuvvDOBiVQ1KB91OscTK2v8tzYMVDF4r011RmSDdqdtagP07WempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lRciM1Y/viKibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwuwwZgf8q9tZBXKPmZOx4COUAVHV1e1wysebsrFHoSRaFri8XVXxTmR5VCSDE6gv7V9H/qH2pmPB63Xy2NMv3QLR8Yj+i4r9vRQWg3CscPD406GXakOR/iatapFSqoBkpkN2cW52cKPcrJvCVRtgdX2cUG58JDyE=

On Thu, Feb 25, 2016 at 2:46 PM, Abhishek Anand
<abhishek.anand.iitg AT gmail.com>
wrote:
> MathClasses has something similar, which I like a lot:
>
> http://www.cs.cornell.edu/~aa755/ROSCoq/coqdoc/MathClasses.misc.decision.html

OK, there's a lot of stuff otherwise in MathClasses that I wish would
make its way into the standard library, too. I just hadn't noticed
that one - though it does seem like it could still use more extension
along the lines I was thinking. (For example, I see and_dec and
or_dec there, but no impl_dec.)
--
Daniel Schepler

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