coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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,
Flavio L. C. de Moura
- Re: [Coq-Club] a claim about prime numbers, Stéphane Glondu
- [Coq-Club] Re: a claim about prime numbers, Adam Megacz
- Re: [Coq-Club] a claim about prime numbers,
Taral
Archive powered by MhonArc 2.6.16.