The Coq mailing list

[David Monniaux <monniaux AT clipper.ens.fr>]

I have a (maybe) naive question: while
(X: Set) (P: X->bool) ~(x: X) (P x)=false -> (EX x: X | (P x)=true)
is obviously false (without a classical axiom), is it possible to prove it
for X=nat ?

We do have an effective procedure for computing such an x: scan all
possible naturals until one fits, which is bound to happen because of the
hypothesis. The question is: is such a procedure definable in Coq?

-- David