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

• ma.bind 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

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

@[reducible, inline]

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

• x.toOption = 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

• ma.tryCatch 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

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

@[always_inline]

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

Equations

• Except.instMonad = 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

• x.run = 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

• ma.bind 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.instMonadLiftExcept {ε : Type u} {m : Type u → Type v} [Monad m] : MonadLift (Except ε) (ExceptT ε m)

Equations

• ExceptT.instMonadLiftExcept = { monadLift := fun {α : Type u} (e : Except ε α) => ExceptT.mk (pure e) }

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

Equations

• ExceptT.instMonadLift = { monadLift := fun {α : Type u} => 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

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

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

Equations

• ExceptT.instMonadFunctor = { monadMap := fun {α : Type u} (f : {β : Type u} → m β → m β) (x : ExceptT ε m α) => f x }

@[always_inline]

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

Equations

• ExceptT.instMonad = 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) [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m)

Equations

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

@[always_inline]

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

Equations

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

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

Equations

• instInhabitedExceptTOfMonad = { default := throw default }

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

Equations

• instMonadExceptOfExcept ε = { throw := fun {α : Type u_2} => Except.error, tryCatch := fun {α : Type u_2} => 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 instMonadControlExceptTOfMonad (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (ExceptT ε m)

Equations

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

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 : Option α) => finalizer; (fun (x : α × β) => x.fst) <$> y

@[always_inline]

instance Id.finally : MonadFinally Id

Equations

• Id.finally = { tryFinally' := fun {α β : Type u_1} (x : Id α) (h : Option α → Id β) => 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.