From 0bd15be1a1fcf237dc897db73efe5220b93a2143 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 21 Oct 2023 06:47:23 -0700
Subject: [PATCH] chore: fix tests output

---
 tests/lean/1616.lean.expected.out             | 38 ++++++------
 tests/lean/jason1.lean.expected.out           | 58 +++++++++----------
 ...syntheticHolesAsPatterns.lean.expected.out | 18 +++---
 3 files changed, 57 insertions(+), 57 deletions(-)

diff --git a/tests/lean/1616.lean.expected.out b/tests/lean/1616.lean.expected.out
index 7f3cc26342..0d1b7beca8 100644
--- a/tests/lean/1616.lean.expected.out
+++ b/tests/lean/1616.lean.expected.out
@@ -1,8 +1,3 @@
-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:24-10:41: error: don't know how to synthesize implicit argument
   @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
 context:
@@ -13,33 +8,28 @@ c : Cover ?m ?m ?m
 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: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: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: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
+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:11-9:19: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m ?m ?m c
+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
@@ -48,3 +38,13 @@ c : Cover ?m ?m ?m
 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: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
diff --git a/tests/lean/jason1.lean.expected.out b/tests/lean/jason1.lean.expected.out
index dc21152680..7be9b76d20 100644
--- a/tests/lean/jason1.lean.expected.out
+++ b/tests/lean/jason1.lean.expected.out
@@ -1,3 +1,31 @@
+jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+Γ✝ : G
+⊢ G
+jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+Γ✝ : G
+⊢ G
 jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
   @EGrfl
     (getCtx
@@ -48,21 +76,7 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
-jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
+jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
   @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
 context:
 G T Tm : Type
@@ -108,17 +122,3 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
diff --git a/tests/lean/syntheticHolesAsPatterns.lean.expected.out b/tests/lean/syntheticHolesAsPatterns.lean.expected.out
index c4e52b5905..f83e52a17c 100644
--- a/tests/lean/syntheticHolesAsPatterns.lean.expected.out
+++ b/tests/lean/syntheticHolesAsPatterns.lean.expected.out
@@ -1,11 +1,3 @@
-syntheticHolesAsPatterns.lean:7:30-7:31: error: don't know how to synthesize placeholder
-context:
-α✝ β : Type
-a✝ : α✝
-x : Fam2 α✝ β
-α : Type
-a : α
-⊢ α
 syntheticHolesAsPatterns.lean:8:30-8:31: error: don't know how to synthesize placeholder
 context:
 α β : Type
@@ -13,9 +5,10 @@ a✝ : α
 x : Fam2 α β
 a n : Nat
 ⊢ Nat
-syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder
+syntheticHolesAsPatterns.lean:7:30-7:31: error: don't know how to synthesize placeholder
 context:
 α✝ β : Type
+a✝ : α✝
 x : Fam2 α✝ β
 α : Type
 a : α
@@ -26,3 +19,10 @@ context:
 x : Fam2 α β
 n a : Nat
 ⊢ Nat
+syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder
+context:
+α✝ β : Type
+x : Fam2 α✝ β
+α : Type
+a : α
+⊢ α