diff options
Diffstat (limited to 'ci/test_stepwise.v')
| -rw-r--r-- | ci/test_stepwise.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/ci/test_stepwise.v b/ci/test_stepwise.v new file mode 100644 index 00000000..3812adbd --- /dev/null +++ b/ci/test_stepwise.v @@ -0,0 +1,22 @@ +Definition trois := 3. (*test-definition*) +Print trois. +Eval compute in 10 * trois * trois. + + + +Lemma easy_proof : forall A : Prop, A -> A. +Proof using . + intros A. + intros proof_of_A. (*test-insert*) + exact proof_of_A. +Qed. (*test-lemma*) + +Lemma false_proof : forall A B : bool, A = B. +Proof. + intros A B. + destruct A. + destruct B. + reflexivity. (*error*) + reflexivity. +Qed. (*test-lemma2*) + |