michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/run/rewriter12): broken test, now ^[ is a token

Browse source
This commit is contained in:
Leonardo de Moura 2015-09-16 08:37:43 -07:00
parent 631b9b3312
commit 68dc39c106
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/rewriter12.lean
View file

@ -3,7 +3,7 @@ open nat
constant f : nat → nat
example (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y :=
by rewrite [▸* at H1, ^[add, nat.rec_on, of_num] at H1, H1]
by rewrite [▸* at H1, ^ [add, nat.rec_on, of_num] at H1, H1]
example (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y :=
by rewrite [▸* at H1, ↑[add, nat.rec_on, of_num] at H1, H1]