fix: tests

leanprover · Dec 22, 2022 · a90afa8 · a90afa8
1 parent 7736c05
commit a90afa8
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/tests/lean/syntheticHolesAsPatterns.lean.expected.out b/tests/lean/syntheticHolesAsPatterns.lean.expected.out
@@ -13,16 +13,16 @@ x : Fam2 α✝ β
 α : Type
 a : α
 ⊢ α
+syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder
+context:
+α β : Type
+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 : α
 ⊢ α
-syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder
-context:
-α β : Type
-x : Fam2 α β
-n a : Nat
-⊢ Nat