The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 27.04.2016 um 19:48 schrieb Guillaume Melquiond:
> You are mixing two kinds of decidability here. (I don't know if there is
> a better way to name them.) One is the excluded-middle property and the
> other is the existence of an algorithm.
Ah, language :) By decider for P I always mean one that goes to +. The 
other property I just call XM.

> Here is a Coq script to make it
> clearer:
>
> Lemma foo : forall n, P n \/ not (P n) -> {P n} + {not (P n)}.
Yes, it seems we were thinking about the same thing : )

Thanks for your explanation,
jonas