diff --git a/tests/lean/rewrite.lean.expected.out b/tests/lean/rewrite.lean.expected.out index 5d1a74f673..cace9e200b 100644 --- a/tests/lean/rewrite.lean.expected.out +++ b/tests/lean/rewrite.lean.expected.out @@ -2,6 +2,7 @@ as bs : List α ⊢ as ++ bs ++ bs = as ++ (bs ++ bs) rewrite.lean:14:20: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression + List.reverse (List.reverse ?m) α : Type _ as bs : List α ⊢ as ++ List.nil ++ List.nil ++ bs ++ bs = as ++ (bs ++ bs)