The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Thu, Sep 01, 2005 at 07:46:13PM +0200, Lionel Elie Mamane wrote:

> Shouldn't all (or most) the things in theories/Logic/Decidable.v
> (and all theorems of the form "Decidable.decidable P" for some P) be
> transparent instead of opaque? The whole point of being decidable is
> that you can _compute_ trough it, right?

Now that I've slept on it, I "see" that I'm confusing constructive and
computable again, the whole distinction Coq makes through Prop/Set,
yada, yada. Except that what I want is to produce a proposition, thus
in Prop. Am I fundamentally breaking the "Coq model" by doing that?

Maybe I shouldn't use " (<=) : nat -> nat -> Prop" for my function's
pre-conditions, but " leB: nat -> nat -> Bool"? This feels somehow
wrong, because it is exactly the computationally *irrelevant* things
I'm making computational, but it should work. I'll try.

-- 
Lionel