diff options
Diffstat (limited to 'ci/test1.v')
| -rw-r--r-- | ci/test1.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/ci/test1.v b/ci/test1.v new file mode 100644 index 00000000..0c4b77fe --- /dev/null +++ b/ci/test1.v @@ -0,0 +1,12 @@ +Definition trois := 3. +Print trois. +Eval compute in 10 * trois * trois. + + + +Lemma easy_proof : (forall A : Prop, A -> A). +Proof using . + intros A. + intros proof_of_A. + exact proof_of_A. +Qed. |