max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove MonadExceptOf from MonadIO

Browse source 
@Kha we currently do not need this feature. We may add it back when needed.
This commit is contained in:
Leonardo de Moura 2020-08-18 15:40:16 -07:00
parent 9519479726
commit b8044fdf97
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/System/IO.lean
View file

@ -68,7 +68,7 @@ constant allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α := arbitra
@[extern "lean_io_initializing"]
constant IO.initializing : IO Bool := arbitrary _
class MonadIO (m : Type → Type) extends HasMonadLiftT IO m, MonadExceptOf IO.Error m
class MonadIO (m : Type → Type) extends HasMonadLiftT IO m
instance : MonadIO IO := {}
@ -78,8 +78,8 @@ an error is returned in the topmost monad. -/
instance ReaderT.monadIO {ρ} (m : Type → Type) [Monad m] [MonadIO m] : MonadIO (ReaderT ρ m) := {}
instance StateT.monadIO {σ} (m : Type → Type) [Monad m] [MonadIO m] : MonadIO (StateT σ m) := {}
def mkMonadIO {m : Type → Type} (lift : forall α, IO α → m α) (mex : MonadExceptOf IO.Error m) :=
@MonadIO.mk m ⟨lift⟩ mex
def mkMonadIO {m : Type → Type} (lift : forall α, IO α → m α) :=
@MonadIO.mk m ⟨lift⟩
namespace IO