chore: MonadExceptCore => MonadExceptOf

src/Init/Control/EState.lean

@@ -116,7 +116,7 @@ instance {δ} [Backtrackable δ σ] : HasOrelse (EStateM ε σ α) :=
 instance : MonadState σ (EStateM ε σ) :=
 { set := @EStateM.set _ _, get := @EStateM.get _ _, modifyGet := @EStateM.modifyGet _ _ }
 
-instance {δ} [Backtrackable δ σ] : MonadExceptCore ε (EStateM ε σ) :=
+instance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) :=
 { throw := @EStateM.throw _ _, catch := @EStateM.catch _ _ _ _ }
 
 @[inline] def adaptState {σ₁ σ₂} (split : σ → σ₁ × σ₂) (merge : σ₁ → σ₂ → σ) (x : EStateM ε σ₁ α) : EStateM ε σ α :=

src/Init/Control/Except.lean

@@ -126,36 +126,36 @@ fun x => ExceptT.mk $ Except.mapError f <$> x
 end ExceptT
 
 /-- An implementation of [MonadError](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Except.html#t:MonadError) -/
-class MonadExceptCore (ε : Type u) (m : Type v → Type w) :=
+class MonadExceptOf (ε : Type u) (m : Type v → Type w) :=
 (throw {α : Type v} : ε → m α)
 (catch {α : Type v} : m α → (ε → m α) → m α)
 
-abbrev throwThe (ε : Type u) {m : Type v → Type w} [MonadExceptCore ε m] {α : Type v} (e : ε) : m α :=
-MonadExceptCore.throw e
+abbrev throwThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (e : ε) : m α :=
+MonadExceptOf.throw e
 
-abbrev catchThe (ε : Type u) {m : Type v → Type w} [MonadExceptCore ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α :=
-MonadExceptCore.catch x handle
+abbrev catchThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α :=
+MonadExceptOf.catch x handle
 
-instance ExceptT.monadExceptParent (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptCore ε₁ m] : MonadExceptCore ε₁ (ExceptT ε₂ m) :=
+instance ExceptT.monadExceptParent (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) :=
 { throw := fun α e        => ExceptT.mk $ throwThe ε₁ e,
   catch := fun α x handle => ExceptT.mk $ catchThe ε₁ x handle }
 
-instance ExceptT.monadExceptSelf (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptCore ε (ExceptT ε m) :=
+instance ExceptT.monadExceptSelf (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) :=
 { throw := fun α e => ExceptT.mk $ pure (Except.error e),
   catch := @ExceptT.catch ε _ _ }
 
-instance (ε) : MonadExceptCore ε (Except ε) :=
+instance (ε) : MonadExceptOf ε (Except ε) :=
 { throw := fun α => Except.error,
   catch := @Except.catch _ }
 
-/-- Similar to `MonadExceptCore`, but `ε` is an outParam for convenience -/
+/-- Similar to `MonadExceptOf`, but `ε` is an outParam for convenience -/
 class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) :=
 (throw {α : Type v} : ε → m α)
 (catch {α : Type v} : m α → (ε → m α) → m α)
 
 export MonadExcept (throw catch)
 
-instance MonadExceptCore.isMonadExcept (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptCore ε m] : MonadExcept ε m :=
+instance MonadExceptOf.isMonadExcept (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m :=
 { throw := fun _ e        => throwThe ε e,
   catch := fun _ x handle => catchThe ε x handle }
 

src/Init/Control/Option.lean

@@ -63,7 +63,7 @@ namespace OptionT
   (do { some a ← ma | (handle ());
         pure a } : m (Option α))
 
-  instance : MonadExceptCore Unit (OptionT m) :=
+  instance : MonadExceptOf Unit (OptionT m) :=
   { throw := fun _ _ => OptionT.fail, catch := @OptionT.catch _ _ }
 
   instance (m out) [MonadRun out m] : MonadRun (fun α => out (Option α)) (OptionT m) :=

src/Init/Control/Reader.lean

@@ -64,7 +64,7 @@ instance [Alternative m] : Alternative (ReaderT ρ m) :=
   failure := @ReaderT.failure _ _ _ _,
   orelse  := @ReaderT.orelse _ _ _ _ }
 
-instance (ε) [Monad m] [MonadExceptCore ε m] : MonadExceptCore ε (ReaderT ρ m) :=
+instance (ε) [Monad m] [MonadExceptOf ε m] : MonadExceptOf ε (ReaderT ρ m) :=
 { throw := fun α => ReaderT.lift ∘ throwThe ε,
   catch := fun α x c r => catchThe ε (x r) (fun e => (c e) r) }
 

src/Init/Control/State.lean

@@ -80,7 +80,7 @@ fun st => do
   (a, st') ← x st;
   pure (a, join st' ctx)
 
-instance (ε) [MonadExceptCore ε m] : MonadExceptCore ε (StateT σ m) :=
+instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) :=
 { throw := fun α => StateT.lift ∘ throwThe ε,
   catch := fun α x c s => catchThe ε (x s) (fun e => c e s) }
 

src/Init/System/IO.lean

@@ -35,7 +35,7 @@ fun s => match x s with
 | EStateM.Result.error ex s => h ex s
 
 instance (ε : Type) : Monad (EIO ε) := inferInstanceAs (Monad (EStateM ε IO.RealWorld))
-instance (ε : Type) : MonadExceptCore ε (EIO ε) := inferInstanceAs (MonadExceptCore ε (EStateM ε IO.RealWorld))
+instance (ε : Type) : MonadExceptOf ε (EIO ε) := inferInstanceAs (MonadExceptOf ε (EStateM ε IO.RealWorld))
 instance (α ε : Type) : HasOrelse (EIO ε α) := ⟨MonadExcept.orelse⟩
 instance {ε : Type} {α : Type} [Inhabited ε] : Inhabited (EIO ε α) :=
 inferInstanceAs (Inhabited (EStateM ε IO.RealWorld α))
@@ -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, MonadExceptCore IO.Error m
+class MonadIO (m : Type → Type) extends HasMonadLiftT IO m, MonadExceptOf IO.Error m
 
 instance : MonadIO IO := {}