Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • 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



Archive powered by MhonArc 2.6.16.

Top of Page