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.
|
