blob: 3812adbddbb465d3449f3a40f95c14e72332f44e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
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*)
|
