From 61a029d9dff1f2aad7ebec242c74ac86212b93fd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Feb 2015 19:21:26 -0800 Subject: [PATCH] fix(tests/lean/rewrite_loop): notation --- tests/lean/rewrite_loop.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/rewrite_loop.lean b/tests/lean/rewrite_loop.lean index cce2d8fbd..945632383 100644 --- a/tests/lean/rewrite_loop.lean +++ b/tests/lean/rewrite_loop.lean @@ -3,5 +3,5 @@ open algebra theorem test {A : Type} [s : comm_ring A] (a b c : A) : a + b + c = a + c + b := begin - rewrite ?add.comm + rewrite *add.comm end