blob: 82096f29bfb37c84333ec340f8eb46d2dbb8b51e (
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
26
27
28
29
30
31
32
33
34
35
36
37
|
(* Some tests of the Search command *)
Search le. (* app nodes *)
Search bool. (* no apps *)
Search (@eq nat). (* complex pattern *)
Search (@eq _ _ true).
Search (@eq _ _ _) true -false. (* andb_prop *)
Search (@eq _ _ _) true -false "prop" -"intro". (* andb_prop *)
Definition newdef := fun x:nat => x.
Goal forall n:nat, n <> newdef n -> newdef n <> n -> False.
cut False.
intros _ n h h'.
Search n. (* search hypothesis *)
Search newdef. (* search hypothesis *)
Search ( _ <> newdef _). (* search hypothesis, pattern *)
Search ( _ <> newdef _) -"h'". (* search hypothesis, pattern *)
1:Search newdef.
2:Search newdef.
Fail 3:Search newdef.
Fail 1-2:Search newdef.
Fail all:Search newdef.
Abort.
Goal forall n (P:nat -> Prop), P n -> ~P n -> False.
intros n P h h'.
Search P. (* search hypothesis also for patterns *)
Search (P _). (* search hypothesis also for patterns *)
Search (P n). (* search hypothesis also for patterns *)
Search (P _) -"h'". (* search hypothesis also for patterns *)
Search (P _) -not. (* search hypothesis also for patterns *)
Abort.
|
