blob: 2f7425bce67ee2e17fe9030b4db899ce40ee6859 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
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.
Lemma foo (n: nat) (P : nat -> Prop):
P n.
Proof.
intros.
refine (nat_ind _ ?[Base] ?[Step] _).
[Base]: { admit. }
[Step]: { admit. }
Abort.
|
