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

chore: remove temporary defs

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-22 17:31:07 -07:00
parent cd5346579b
commit f1dd85e8a3
1 changed files with 0 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Control/Except.lean
View file

@ -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 }