Documentation

Init.Control.Except

@[inline]
def Except.pure {ε : Type u} {α : Type u_1} (a : α) :
Except ε α
Equations
@[inline]
def Except.map {ε : Type u} {α : Type u_1} {β : Type u_2} (f : αβ) :
Except ε αExcept ε β
Equations
@[simp]
theorem Except.map_id {ε : Type u} {α : Type u_1} :
@[inline]
def Except.mapError {ε : Type u} {ε' : Type u_1} {α : Type u_2} (f : εε') :
Except ε αExcept ε' α
Equations
@[inline]
def Except.bind {ε : Type u} {α : Type u_1} {β : Type u_2} (ma : Except ε α) (f : αExcept ε β) :
Except ε β
Equations
@[inline]
def Except.toBool {ε : Type u} {α : Type u_1} :
Except ε αBool
Equations
@[inline]
def Except.toOption {ε : Type u} {α : Type u_1} :
Except ε αOption α
Equations
@[inline]
def Except.tryCatch {ε : Type u} {α : Type u_1} (ma : Except ε α) (handle : εExcept ε α) :
Except ε α
Equations
def Except.orElseLazy {ε : Type u} {α : Type u_1} (x : Except ε α) (y : UnitExcept ε α) :
Except ε α
Equations
instance Except.instMonadExcept {ε : Type u} :
Equations
  • Except.instMonadExcept = Monad.mk
noncomputable def ExceptT (ε : Type u) (m : Type uType v) (α : Type u) :
Type v
Equations
@[inline]
def ExceptT.mk {ε : Type u} {m : Type uType v} {α : Type u} (x : m (Except ε α)) :
ExceptT ε m α
Equations
@[inline]
def ExceptT.run {ε : Type u} {m : Type uType v} {α : Type u} (x : ExceptT ε m α) :
m (Except ε α)
Equations
@[inline]
def ExceptT.pure {ε : Type u} {m : Type uType v} [inst : Monad m] {α : Type u} (a : α) :
ExceptT ε m α
Equations
@[inline]
def ExceptT.bindCont {ε : Type u} {m : Type uType v} [inst : Monad m] {α : Type u} {β : Type u} (f : αExceptT ε m β) :
Except ε αm (Except ε β)
Equations
@[inline]
def ExceptT.bind {ε : Type u} {m : Type uType v} [inst : Monad m] {α : Type u} {β : Type u} (ma : ExceptT ε m α) (f : αExceptT ε m β) :
ExceptT ε m β
Equations
@[inline]
def ExceptT.map {ε : Type u} {m : Type uType v} [inst : Monad m] {α : Type u} {β : Type u} (f : αβ) (x : ExceptT ε m α) :
ExceptT ε m β
Equations
@[inline]
def ExceptT.lift {ε : Type u} {m : Type uType v} [inst : Monad m] {α : Type u} (t : m α) :
ExceptT ε m α
Equations
instance ExceptT.instMonadLiftExceptExceptT {ε : Type u} {m : Type uType v} [inst : Monad m] :
Equations
  • ExceptT.instMonadLiftExceptExceptT = { monadLift := fun {α} e => ExceptT.mk (pure e) }
instance ExceptT.instMonadLiftExceptT {ε : Type u} {m : Type uType v} [inst : Monad m] :
Equations
  • ExceptT.instMonadLiftExceptT = { monadLift := fun {α} => ExceptT.lift }
@[inline]
def ExceptT.tryCatch {ε : Type u} {m : Type uType v} [inst : Monad m] {α : Type u} (ma : ExceptT ε m α) (handle : εExceptT ε m α) :
ExceptT ε m α
Equations
instance ExceptT.instMonadFunctorExceptT {ε : Type u} {m : Type uType v} :
Equations
  • ExceptT.instMonadFunctorExceptT = { monadMap := fun {α} f x => f (Except ε α) x }
instance ExceptT.instMonadExceptT {ε : Type u} {m : Type uType v} [inst : Monad m] :
Monad (ExceptT ε m)
Equations
  • ExceptT.instMonadExceptT = Monad.mk
@[inline]
def ExceptT.adapt {ε : Type u} {m : Type uType v} [inst : Monad m] {ε' : Type u} {α : Type u} (f : εε') :
ExceptT ε m αExceptT ε' m α
Equations
instance instMonadExceptOfExceptT (m : Type uType v) (ε₁ : Type u) (ε₂ : Type u) [inst : Monad m] [inst : MonadExceptOf ε₁ m] :
MonadExceptOf ε₁ (ExceptT ε₂ m)
Equations
instance instMonadExceptOfExceptT_1 (m : Type uType v) (ε : Type u) [inst : Monad m] :
Equations
instance instInhabitedExceptT {m : Type u_1Type u_2} {ε : Type u_1} {α : Type u_1} [inst : Monad m] [inst : Inhabited ε] :
Inhabited (ExceptT ε m α)
Equations
  • instInhabitedExceptT = { default := throw default }
instance instMonadExceptOfExcept (ε : Type u_1) :
Equations
@[inline]
def MonadExcept.orelse' {ε : Type u} {m : Type vType w} [inst : MonadExcept ε m] {α : Type v} (t₁ : m α) (t₂ : m α) (useFirstEx : optParam Bool true) :
m α
Equations
@[inline]
def observing {ε : Type u} {α : Type u} {m : Type uType v} [inst : Monad m] [inst : MonadExcept ε m] (x : m α) :
m (Except ε α)
Equations
def liftExcept {ε : Type u_1} {m : Type u_2Type u_3} {α : Type u_2} [inst : MonadExceptOf ε m] [inst : Pure m] :
Except ε αm α
Equations
instance instMonadControlExceptT (ε : Type u) (m : Type uType v) [inst : Monad m] :
Equations
@[inline]
def tryFinally {m : Type uType v} {α : Type u} {β : Type u} [inst : MonadFinally m] [inst : Functor m] (x : m α) (finalizer : m β) :
m α
Equations
Equations
  • Id.finally = { tryFinally' := fun {α β} x h => let a := x; let b := h (some x); pure (a, b) }
instance ExceptT.finally {m : Type uType v} {ε : Type u} [inst : MonadFinally m] [inst : Monad m] :
Equations