aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/SearchRewrite.v
blob: 53d043c6816d0f51bce6e9652136b9d7be835773 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
(* Some tests of the SearchRewrite command *)

SearchRewrite (_+0). 			(* left *)
SearchRewrite (0+_). 			(* right *)

Definition newdef := fun x:nat => x.

Goal forall n:nat, n = newdef n -> False.
  intros n h.
  SearchRewrite (newdef _).
  SearchRewrite n.                (* use hypothesis for patterns *)
  SearchRewrite (newdef n).       (* use hypothesis for patterns *)
Abort.