0

I have entered the following code in CoqIde:

Require Export Classical. 
Require Export Description. 



Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.

Theorem classical_definite_description :
 forall (A : Type) (P : A->Prop), inhabited A ->
{ x : A | (exists! x : A, P x) -> P x }.

The message Nested proofs are not allowed unless you turn option Nested Proofs Allowed on. is produced. How can I turn on the option Nested Proofs Allowed?

1 Answer 1

1

You probably want to change the keyword Theorem for excluded_middle_informative to Axiom, since this is what it is (you don't provide a proof for it).

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.