From ddbca07a0f0cb706856cd0f744d7ec9ba2e59ef5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 Oct 2020 15:13:38 -0700 Subject: [PATCH] chore: fix test output --- tests/lean/rewrite.lean.expected.out | 1 + 1 file changed, 1 insertion(+) 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)