The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

I'm told that "(P n \/ ~ P n)" is confusing in the paragraph
below.

> This suggests another definition of "deciding" which is the ability to
> "approximate" the truth of (P n \/ ~ P n), in the sense of being able
> to locally produce a witness of (P n \/ ~ P n) in the context of any
> other proof p that relies on (P n \/ ~ P n). (...)

It should be read it either as Q \/ ~Q for general Q, or as
({n | ~P n} + {forall n, P n}) for the P that was under discussion
(ignoring the ability to then extract an "option nat" from it, that
the other message discusses).

Sorry.

Hugo