blob: 0ed5b524f37bf1e9f5260d008f2ac439ad6bace9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* Testing forward reasoning *)
Goal 0=0.
Fail assert (_ = _).
eassert (_ = _)by reflexivity.
eassumption.
Qed.
Goal 0=0.
Fail set (S ?[nl]).
eset (S ?[n]).
remember (S ?n) as x.
instantiate (n:=0).
Fail remember (S (S _)).
eremember (S (S ?[x])).
instantiate (x:=0).
reflexivity.
Qed.
|
