@[inline]

def Except.pure {ε : Type u} {α : Type u_1} (a : α) : Except ε α

Equations

• Except.pure a = Except.ok a

@[inline]

def Except.map {ε : Type u} {α : Type u_1} {β : Type u_2} (f : α → β) : Except ε α → Except ε β

Equations

• Except.map f x = match x with | Except.error err => Except.error err | Except.ok v => Except.ok (f v)

@[simp]

theorem Except.map_id {ε : Type u} {α : Type u_1} : Except.map id = id

@[inline]

def Except.mapError {ε : Type u} {ε' : Type u_1} {α : Type u_2} (f : ε → ε') : Except ε α → Except ε' α

Equations

• Except.mapError f x = match x with | Except.error err => Except.error (f err) | Except.ok v => Except.ok v

@[inline]

def Except.bind {ε : Type u} {α : Type u_1} {β : Type u_2} (ma : Except ε α) (f : α → Except ε β) : Except ε β

Equations

• Except.bind ma f = match ma with | Except.error err => Except.error err | Except.ok v => f v

@[inline]

def Except.toBool {ε : Type u} {α : Type u_1} : Except ε α → Bool

Returns true if the value is Except.ok, false otherwise.

Equations

• Except.toBool x = match x with | Except.ok a => true | Except.error a => false

@[inline, reducible]

abbrev Except.isOk {ε : Type u} {α : Type u_1} : Except ε α → Bool

Equations

• Except.isOk = Except.toBool

@[inline]

def Except.toOption {ε : Type u} {α : Type u_1} : Except ε α → Option α

Equations

• Except.toOption x = match x with | Except.ok a => some a | Except.error a => none

@[inline]

def Except.tryCatch {ε : Type u} {α : Type u_1} (ma : Except ε α) (handle : ε → Except ε α) : Except ε α

Equations

• Except.tryCatch ma handle = match ma with | Except.ok a => Except.ok a | Except.error e => handle e

def Except.orElseLazy {ε : Type u} {α : Type u_1} (x : Except ε α) (y : Unit → Except ε α) : Except ε α

Equations

• Except.orElseLazy x y = match x with | Except.ok a => Except.ok a | Except.error a => y ()

@[always_inline]

instance Except.instMonadExcept {ε : Type u} : Monad (Except ε)

Equations

• Except.instMonadExcept = Monad.mk

def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v

Equations

• ExceptT ε m α = m (Except ε α)

@[inline]

def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) : ExceptT ε m α

Equations

• ExceptT.mk x = x

@[inline]

def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α)

Equations

• ExceptT.run x = x

@[inline]

def ExceptT.pure {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (a : α) : ExceptT ε m α

Equations

• ExceptT.pure a = ExceptT.mk (pure (Except.ok a))

@[inline]

def ExceptT.bindCont {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β)

Equations

• ExceptT.bindCont f x = match x with | Except.ok a => f a | Except.error e => pure (Except.error e)

@[inline]

def ExceptT.bind {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m β

Equations

• ExceptT.bind ma f = ExceptT.mk (ma >>= ExceptT.bindCont f)

@[inline]

def ExceptT.map {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β

Equations

• ExceptT.map f x = ExceptT.mk do let a ← x match a with | Except.ok a => pure (Except.ok (f a)) | Except.error e => pure (Except.error e)

@[inline]

def ExceptT.lift {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (t : m α) : ExceptT ε m α

Equations

• ExceptT.lift t = ExceptT.mk (Except.ok <$> t)

@[always_inline]

instance ExceptT.instMonadLiftExceptExceptT {ε : Type u} {m : Type u → Type v} [Monad m] : MonadLift (Except ε) (ExceptT ε m)

Equations

• ExceptT.instMonadLiftExceptExceptT = { monadLift := fun {α} e => ExceptT.mk (pure e) }

instance ExceptT.instMonadLiftExceptT {ε : Type u} {m : Type u → Type v} [Monad m] : MonadLift m (ExceptT ε m)

Equations

• ExceptT.instMonadLiftExceptT = { monadLift := fun {α} => ExceptT.lift }

@[inline]

def ExceptT.tryCatch {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α

Equations

• ExceptT.tryCatch ma handle = ExceptT.mk do let res ← ma match res with | Except.ok a => pure (Except.ok a) | Except.error e => handle e

instance ExceptT.instMonadFunctorExceptT {ε : Type u} {m : Type u → Type v} : MonadFunctor m (ExceptT ε m)

Equations

• ExceptT.instMonadFunctorExceptT = { monadMap := fun {α} f x => f (Except ε α) x }

@[always_inline]

instance ExceptT.instMonadExceptT {ε : Type u} {m : Type u → Type v} [Monad m] : Monad (ExceptT ε m)

Equations

• ExceptT.instMonadExceptT = Monad.mk

@[inline]

def ExceptT.adapt {ε : Type u} {m : Type u → Type v} [Monad m] {ε' : Type u} {α : Type u} (f : ε → ε') : ExceptT ε m α → ExceptT ε' m α

Equations

• ExceptT.adapt f x = ExceptT.mk (Except.mapError f <$> x)

@[always_inline]

instance instMonadExceptOfExceptT (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m)

Equations

• instMonadExceptOfExceptT m ε₁ ε₂ = { throw := fun {α} e => ExceptT.mk (throwThe ε₁ e), tryCatch := fun {α} x handle => ExceptT.mk (tryCatchThe ε₁ x handle) }

@[always_inline]

instance instMonadExceptOfExceptT_1 (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m)

Equations

• instMonadExceptOfExceptT_1 m ε = { throw := fun {α} e => ExceptT.mk (pure (Except.error e)), tryCatch := fun {α} => ExceptT.tryCatch }

instance instInhabitedExceptT {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} [Monad m] [Inhabited ε] : Inhabited (ExceptT ε m α)

Equations

• instInhabitedExceptT = { default := throw default }

instance instMonadExceptOfExcept (ε : Type u_1) : MonadExceptOf ε (Except ε)

Equations

• instMonadExceptOfExcept ε = { throw := fun {α} => Except.error, tryCatch := fun {α} => Except.tryCatch }

@[inline]

def MonadExcept.orelse' {ε : Type u} {m : Type v → Type w} [MonadExcept ε m] {α : Type v} (t₁ : m α) (t₂ : m α) (useFirstEx : optParam Bool true) : m α

Alternative orelse operator that allows to select which exception should be used. The default is to use the first exception since the standard orelse uses the second.

Equations

• MonadExcept.orelse' t₁ t₂ useFirstEx = tryCatch t₁ fun e₁ => tryCatch t₂ fun e₂ => throw (if useFirstEx = true then e₁ else e₂)

@[inline]

def observing {ε : Type u} {α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) : m (Except ε α)

Equations

• observing x = tryCatch (do let a ← x pure (Except.ok a)) fun ex => pure (Except.error ex)

def liftExcept {ε : Type u_1} {m : Type u_2 → Type u_3} {α : Type u_2} [MonadExceptOf ε m] [Pure m] : Except ε α → m α

Equations

• liftExcept x = match x with | Except.ok a => pure a | Except.error e => throw e

instance instMonadControlExceptT (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (ExceptT ε m)

Equations

• instMonadControlExceptT ε m = { stM := Except ε, liftWith := fun {α} f => liftM (f fun {β} x => ExceptT.run x), restoreM := fun {α} x => x }

class MonadFinally (m : Type u → Type v) : Type (max (u + 1) v)

• tryFinally' : {α β : Type u} → m α → (Option α → m β) → m (α × β)

  tryFinally' x f runs x and then the "finally" computation f. When x succeeds with a : α, f (some a) is returned. If x fails for m's definition of failure, f none is returned. Hence tryFinally' can be thought of as performing the same role as a finally block in an imperative programming language.

@[inline]

def tryFinally {m : Type u → Type v} {α : Type u} {β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α

Execute x and then execute finalizer even if x threw an exception

Equations

• tryFinally x finalizer = let y := tryFinally' x fun x => finalizer; (fun x => x.fst) <$> y

@[always_inline]

instance Id.finally : MonadFinally Id

Equations

• Id.finally = { tryFinally' := fun {α β} x h => let a := x; let b := h (some x); pure (a, b) }

@[always_inline]

instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m] [Monad m] : MonadFinally (ExceptT ε m)

Equations

• One or more equations did not get rendered due to their size.