From 7daeb7fffd2ae897eb960cede38a8de528c23646 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 11 Nov 2020 07:18:49 -0800
Subject: [PATCH] chore: fix test

---
 tests/lean/Reformat.lean.expected.out | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/tests/lean/Reformat.lean.expected.out b/tests/lean/Reformat.lean.expected.out
index baa9dd9475..7922d9a53d 100644
--- a/tests/lean/Reformat.lean.expected.out
+++ b/tests/lean/Reformat.lean.expected.out
@@ -147,15 +147,6 @@ theorem natAddZero (n : Nat) : n + 0 = n :=
 theorem optParamEq (α : Sort u) (default : α) : optParam α default = α :=
   rfl
 
-/--Like `by applyInstance`, but not dependent on the tactic framework. -/
-@[reducible]
-def inferInstance {α : Type u} [i : α] : α :=
-  i
-
-@[reducible]
-def inferInstanceAs (α : Type u) [i : α] : α :=
-  i
-
 @[extern c inline "#1 || #2"]
 def strictOr (b₁ b₂ : Bool) :=
   b₁ || b₂