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