From f1dd85e8a3627896d643dec26399be8bbd66247c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Oct 2020 17:31:07 -0700 Subject: [PATCH] chore: remove temporary defs --- src/Init/Control/Except.lean | 6 ------ 1 file changed, 6 deletions(-) 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 }