coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland
Date: Sun, 25 Jan 2015 03:01:17 +0200

A little bit unpolished, I believe. (For example, prime_infinitude follows from prime_infinitude_0, probably can be structured more nicely etc.)

And, oops, I missed the part when you asked for calculation of exact such prime. The proof can be remade for this purpose but I will leave that for someone else or for February when I have more free time.

On Sun, Jan 25, 2015 at 2:54 AM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

There it is. You can skip prime_infinitude and prime_infinitude_0.

To unsubscribe reply with "Nesūti spamu, ķēmīgais rausi!" in the subject heading.

Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Abhishek Anand, 01/25/2015
- Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Ilmārs Cīrulis, 01/25/2015
  - Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Ilmārs Cīrulis, 01/25/2015
    - Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Ilmārs Cīrulis, 01/27/2015
      - Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Abhishek Anand, 01/27/2015
        
        Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Ilmārs Cīrulis, 01/30/2015
        
        Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Abhishek Anand, 01/30/2015
        
        Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Ilmārs Cīrulis, 01/31/2015