diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 5175005772..14311dc3d3 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -136,9 +136,6 @@ class MonadExceptOf (ε : Type u) (m : Type v → Type w) := 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} [MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α := -MonadExceptOf.tryCatch x handle - abbrev tryCatchThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α := MonadExceptOf.tryCatch x handle @@ -161,9 +158,6 @@ class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) := export MonadExcept (throw tryCatch) -abbrev MonadExcept.«catch» {ε : Type u} {m : Type v → Type w} [MonadExcept ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α := -MonadExcept.tryCatch x handle - instance MonadExceptOf.isMonadExcept (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m := { throw := fun _ e => throwThe ε e, tryCatch := fun _ x handle => tryCatchThe ε x handle }