From afed2bb8271a27edbcef4e55717b13551c41e37b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 21 Aug 2020 12:06:16 -0700
Subject: [PATCH] chore: remove dead code

`StateRefT` doesn't need a `MonadIO` instance anymore.
---
 src/Lean/Elab/Command.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 9e06460a1a..488558656b 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -93,10 +93,6 @@ private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : M
 let ref := getBetterRef ref ctx.macroStack;
 mkMessageAux ctx ref (addMacroStack (toString err) ctx.macroStack) MessageSeverity.error
 
--- This instance is needed for StateRefT
-instance monadIOAux : MonadIO (EIO Exception) :=
-{ liftIO := fun _ x => adaptExcept (fun ex => Exception.error { fileName := "<unavaiable>", pos := ⟨0, 0⟩, data := toString ex }) x }
-
 @[inline] def liftEIO {α} (x : EIO Exception α) : CommandElabM α :=
 liftM x