diff options
| author | Erik Martin-Dorel | 2020-05-04 22:02:42 +0200 |
|---|---|---|
| committer | GitHub | 2020-05-04 22:02:42 +0200 |
| commit | 24e1c5ae3dec16c972babcf44786eb7eff3c6b53 (patch) | |
| tree | 03e9d25be79e97fbc6b9ba42cdae2e892617522b /ci/test_stepwise.v | |
| parent | 23db83dc4141d89530f6381ba49f56399682d4e0 (diff) | |
| parent | 63dc6a6bc23f2eff3e3c3bbee9e79d4097d8f139 (diff) | |
Merge pull request #486 from ProofGeneral/coq-tests-for-master
Coq tests for master
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*) + |