blob: 2ee8a0d1843cd5ad78821af03b10c03f074629da (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* Some tests of the Search command *)
SearchHead le. (* app nodes *)
SearchHead bool. (* no apps *)
SearchHead (@eq nat). (* complex pattern *)
Definition newdef := fun x:nat => x = x.
Goal forall n:nat, newdef n -> False.
intros n h.
SearchHead newdef. (* search hypothesis *)
Abort.
Goal forall n (P:nat -> Prop), P n -> False.
intros n P h.
SearchHead P. (* search hypothesis also for patterns *)
Abort.
|
