aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/SearchHead.v
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.