coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] a claim about prime numbers

From: St�phane Lescuyer <stephane.lescuyer AT inria.fr>
To: "Flavio L. C. de Moura" <flaviomoura AT unb.br>
Cc: Taral <taralx AT gmail.com>, coq-club AT inria.fr
Subject: Re: [Coq-Club] a claim about prime numbers
Date: Sat, 22 May 2010 23:27:27 +0200

> So, the problem is the number j because I believe that its existence is
> not enough to build a proof in Coq. It is necessary to have a way to
> build j, isn't it?
>

Well nothing prevents you from *computing* this j, because all
properties you consider here are decidable. So really intuitionistic
logic is not an obstacle here.

S.
--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06

[Coq-Club] a claim about prime numbers, Flavio L. C. de Moura
- Re: [Coq-Club] a claim about prime numbers, Taral
  - Re: [Coq-Club] a claim about prime numbers, Flavio L. C. de Moura
    - Re: [Coq-Club] a claim about prime numbers, St�phane Lescuyer
- Re: [Coq-Club] a claim about prime numbers, Stéphane Glondu
- [Coq-Club] Re: a claim about prime numbers, Adam Megacz