From ebc32af2e606deef0d7b437e67f24c20ed866818 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 15 May 2023 13:23:38 -0700
Subject: [PATCH] chore: fix flaky test

---
 tests/lean/1616.lean.expected.out | 50 +++++++++++++++----------------
 1 file changed, 25 insertions(+), 25 deletions(-)

diff --git a/tests/lean/1616.lean.expected.out b/tests/lean/1616.lean.expected.out
index ec2c50c73e..7f3cc26342 100644
--- a/tests/lean/1616.lean.expected.out
+++ b/tests/lean/1616.lean.expected.out
@@ -1,33 +1,13 @@
-1616.lean:9:31-9:38: error: don't know how to synthesize implicit argument
-  @Cover.left ?m ?m ?m ?m ?m c
-context:
-c : Cover ?m ?m ?m
-⊢ Type u_1
 1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
   @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
 context:
 c : Cover ?m ?m ?m
 ⊢ List ?m
-1616.lean:10:32-10:40: error: don't know how to synthesize implicit argument
-  @Cover.right ?m ?m ?m ?m ?m c
-context:
-c : Cover ?m ?m ?m
-⊢ Type u_1
 1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
   @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
 context:
 c : Cover ?m ?m ?m
-⊢ List ?m
-1616.lean:9:11-9:19: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m ?m ?m c
-context:
-c : Cover ?m ?m ?m
 ⊢ Type u_1
-1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
-context:
-c : Cover ?m ?m ?m
-⊢ List ?m
 1616.lean:10:12-10:20: error: don't know how to synthesize implicit argument
   @Linear ?m ?m ?m ?m c
 context:
@@ -37,14 +17,34 @@ c : Cover ?m ?m ?m
   @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
 context:
 c : Cover ?m ?m ?m
-⊢ Type u_1
-1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
-  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
-context:
-c : Cover ?m ?m ?m
 ⊢ List ?m
 1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
   @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
 context:
 c : Cover ?m ?m ?m
+⊢ List ?m
+1616.lean:9:31-9:38: error: don't know how to synthesize implicit argument
+  @Cover.left ?m ?m ?m ?m ?m c
+context:
+c : Cover ?m ?m ?m
+⊢ Type u_1
+1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
+  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
+context:
+c : Cover ?m ?m ?m
+⊢ List ?m
+1616.lean:10:32-10:40: error: don't know how to synthesize implicit argument
+  @Cover.right ?m ?m ?m ?m ?m c
+context:
+c : Cover ?m ?m ?m
+⊢ Type u_1
+1616.lean:9:11-9:19: error: don't know how to synthesize implicit argument
+  @Linear ?m ?m ?m ?m c
+context:
+c : Cover ?m ?m ?m
+⊢ Type u_1
+1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
+  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
+context:
+c : Cover ?m ?m ?m
 ⊢ Type u_1