From 6f096e0f0dd0403b63b2bf8338e6774abcdf539b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 16 Jun 2022 13:33:35 +0200
Subject: [PATCH] chore: fix tests

---
 tests/lean/Reformat/Input.lean       | 12 +++---------
 tests/lean/StxQuot.lean.expected.out |  4 ++--
 2 files changed, 5 insertions(+), 11 deletions(-)

diff --git a/tests/lean/Reformat/Input.lean b/tests/lean/Reformat/Input.lean
index deb4838c36..43649bfc63 100644
--- a/tests/lean/Reformat/Input.lean
+++ b/tests/lean/Reformat/Input.lean
@@ -186,13 +186,9 @@ class Inhabited (α : Sort u) :=
 opaque arbitrary (α : Sort u) [s : Inhabited α] : α :=
   @Inhabited.default α s
 
-instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) := {
-  default := fun _ => arbitrary β
-}
+instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) := {default := fun _ => arbitrary β}
 
-instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) := {
-  default := fun a => arbitrary (β a)
-}
+instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) := {default := fun a => arbitrary (β a)}
 
 /-- Universe lifting operation from Sort to Type -/
 structure PLift (α : Sort u) : Type u :=
@@ -210,9 +206,7 @@ structure PointedType :=
   (type : Type u)
   (val : type)
 
-instance : Inhabited PointedType.{u} := {
-  default := { type := PUnit.{u+1}, val := ⟨⟩ }
-}
+instance : Inhabited PointedType.{u} := {default := { type := PUnit.{u+1}, val := ⟨⟩ }}
 
 /-- Universe lifting operation -/
 structure ULift.{r, s} (α : Type s) : Type (max s r) :=
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 7ff382d7b6..d6d477193c 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -32,8 +32,8 @@ StxQuot.lean:18:15: error: expected term
 "`a._@.UnhygienicMain._hyg.1"
 "(Term.explicitUniv `a._@.UnhygienicMain._hyg.1 \".{\" [(num \"0\")] \"}\")"
 "#[(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" (num \"1\")), (Term.matchAlt \"|\" [[(Term.hole \"_\")]] \"=>\" (num \"2\"))]"
-"(Term.structInst\n \"{\"\n []\n [(group\n   (Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1)\n   [])]\n (Term.optEllipsis [])\n [\":\" `a._@.UnhygienicMain._hyg.1]\n \"}\")"
-"(Term.structInst\n \"{\"\n []\n [(group\n   (Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1)\n   [])]\n (Term.optEllipsis [])\n []\n \"}\")"
+"(Term.structInst\n \"{\"\n []\n [(Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1)]\n (Term.optEllipsis [])\n [\":\" `a._@.UnhygienicMain._hyg.1]\n \"}\")"
+"(Term.structInst\n \"{\"\n []\n [(Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1)]\n (Term.optEllipsis [])\n []\n \"}\")"
 "(Command.section \"section\" [])"
 "(Command.section \"section\" [`foo._@.UnhygienicMain._hyg.1])"
 "(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n \"with\"\n (Term.matchAlts\n  [(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" `b._@.UnhygienicMain._hyg.1)\n   (Term.matchAlt\n    \"|\"\n    [[(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (num \"1\"))]]\n    \"=>\"\n    («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (num \"1\")))]))"