From 68dc39c1067ba1d1cf17684b7c8ea6d8c19579f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 16 Sep 2015 08:37:43 -0700 Subject: [PATCH] fix(tests/lean/run/rewriter12): broken test, now `^[` is a token --- tests/lean/run/rewriter12.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/rewriter12.lean b/tests/lean/run/rewriter12.lean index e20076f20..82d0c807e 100644 --- a/tests/lean/run/rewriter12.lean +++ b/tests/lean/run/rewriter12.lean @@ -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]