blob: ed035f52130cb831872fc2e2c09d01b03da85253 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Goal forall A B, B \/ A -> A \/ B.
Proof.
intros * [HB | HA].
2: {
left.
exact HA.
Fail right. (* No such goal. Try unfocusing with "}". *)
}
Fail 2: { (* Non-existent goal. *)
idtac. (* The idtac is to get a dot, so that IDEs know to stop there. *)
1:{ (* Syntactic test: no space before bracket. *)
right.
exact HB.
Fail Qed.
}
Qed.
|
