# Documentation

## Lake.Util.EStateT

inductive Lake.EResult (ε : Type u) (σ : Type v) (α : Type w) :
Type (max u v w)

EResult ε σ α is equivalent to Except ε α × σ, but using a single combined inductive yields a more efficient data representation.

• ok: {ε : Type u} → {σ : Type v} → {α : Type w} → ασLake.EResult ε σ α

A success value of type α, and a new state σ.

• error: {ε : Type u} → {σ : Type v} → {α : Type w} → εσLake.EResult ε σ α

A failure value of type ε, and a new state σ.

Instances For
instance Lake.instInhabitedEResult {α : Type u_1} {σ : Type u_2} {ε : Type u_3} [] [] :
Equations
instance Lake.instInhabitedEResult_1 {ε : Type u_1} {σ : Type u_2} {α : Type u_3} [] [] :
Equations
@[inline]
def Lake.EResult.state {ε : Type u_1} {σ : Type u_2} {α : Type u_3} :
Lake.EResult ε σ ασ

Extract the state σ from a EResult ε σ α.

Equations
• x.state = match x with | => s | => s
Instances For
@[inline]
def Lake.EResult.modifyState {σ : Type u_1} {σ' : Type u_2} {ε : Type u_3} {α : Type u_4} (f : σσ') :
Lake.EResult ε σ αLake.EResult ε σ' α
Equations
Instances For
@[inline]
def Lake.EResult.setState {σ' : Type u_1} {ε : Type u_2} {σ : Type u_3} {α : Type u_4} (s : σ') (r : Lake.EResult ε σ α) :
Lake.EResult ε σ' α
Equations
Instances For
@[inline]
def Lake.EResult.toProd {ε : Type u_1} {σ : Type u_2} {α : Type u_3} :
Lake.EResult ε σ αExcept ε α × σ

Convert a EResult ε σ α into Except ε α × σ.

Equations
• x.toProd = match x with | => (, s) | => (, s)
Instances For
@[inline]
def Lake.EResult.toProd? {ε : Type u_1} {σ : Type u_2} {α : Type u_3} :
Lake.EResult ε σ α × σ

Convert an EResult ε σ α into Option α × σ, discarding the exception contents.

Equations
• x.toProd? = match x with | => (some a, s) | => (none, s)
Instances For
@[inline]
def Lake.EResult.result? {ε : Type u_1} {σ : Type u_2} {α : Type u_3} :
Lake.EResult ε σ α

Extract the result α from a EResult ε σ α.

Equations
Instances For
@[inline]
def Lake.EResult.error? {ε : Type u_1} {σ : Type u_2} {α : Type u_3} :
Lake.EResult ε σ α

Extract the error ε from a EResult ε σ α.

Equations
• x.error? = match x with | => some e | x => none
Instances For
@[inline]
def Lake.EResult.toExcept {ε : Type u_1} {σ : Type u_2} {α : Type u_3} :
Lake.EResult ε σ αExcept ε α

Convert an EResult ε σ α into Except ε α, discarding its state.

Equations
Instances For
@[inline]
def Lake.EResult.map {α : Type u_1} {β : Type u_2} {ε : Type u_3} {σ : Type u_4} (f : αβ) :
Lake.EResult ε σ αLake.EResult ε σ β
Equations
Instances For
instance Lake.instFunctorEResult {ε : Type u_1} {σ : Type u_2} :
Equations
• Lake.instFunctorEResult = { map := fun {α β : Type u_3} => Lake.EResult.map, mapConst := fun {α β : Type u_3} => Lake.EResult.map }
def Lake.EStateT (ε : Type u) (σ : Type v) (m : Type (max u v w) → Type x) (α : Type w) :
Type (max v x)

EStateT ε σ m is a combined error and state monad transformer, equivalent to ExceptT ε (StateT σ m) but more efficient.

Equations
Instances For
instance Lake.EStateT.instInhabitedOfPure {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [] [Pure m] :
Inhabited (Lake.EStateT ε σ m α)
Equations
@[inline]
def Lake.EStateT.run {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max u v w) → Type u_1} (init : σ) (self : Lake.EStateT ε σ m α) :
m (Lake.EResult ε σ α)

Execute an EStateT on initial state init to get an EResult result.

Equations
Instances For
@[inline]
def Lake.EStateT.run' {ε : Type u} {α : Type w} {m : Type (max u w) → Type u_1} {σ : Type (max u w)} [] (init : σ) (x : Lake.EStateT ε σ m α) :
m (Except ε α)

Execute an EStateT on initial state init to get an Except result, discarding the final state.

Equations
Instances For
@[inline]
def Lake.EStateT.toStateT {m : Type u → Type u_1} {ε : Type u} {σ : Type u} {α : Type u} [] (x : Lake.EStateT ε σ m α) :
StateT σ m (Except ε α)

Convert an EStateT to a StateT, returning an Except result.

Equations
• x.toStateT s = Lake.EResult.toProd <$> x s Instances For @[inline] def Lake.EStateT.toStateT? {m : Type u → Type u_1} {ε : Type u} {σ : Type u} {α : Type u} [] (x : Lake.EStateT ε σ m α) : StateT σ m () Convert an EStateT to a StateT, returning an Option result. Equations • x.toStateT? s = Lake.EResult.toProd? <$> x s
Instances For
@[inline]
def Lake.EStateT.run? {σ : Type v} {α : Type w} {m : Type (max v w) → Type u_1} {ε : Type (max v w)} [] (init : σ) (x : Lake.EStateT ε σ m α) :
m ( × σ)

Execute an EStateT on initial state init to get an Option result, discarding the exception contents.

Equations
Instances For
@[inline]
def Lake.EStateT.run?' {m : Type u → Type u_1} {ε : Type u} {σ : Type u} {α : Type u} [] (init : σ) (x : Lake.EStateT ε σ m α) :
m ()

Execute an EStateT on initial state init to get an Option result, discarding the final state.

Equations
Instances For
@[inline]
def Lake.EStateT.catchExceptions {m : Type u → Type u_1} {ε : Type u} {σ : Type u} {α : Type u} [] (x : Lake.EStateT ε σ m α) (h : εStateT σ m α) :
StateT σ m α
Equations
• x.catchExceptions h s = do let __do_liftx s match __do_lift with | => pure (a, s) | => h e s
Instances For
@[inline]
def Lake.EStateT.lift {m : Type u → Type u_1} {ε : Type u} {σ : Type u} {α : Type u} [] (x : m α) :
Lake.EStateT ε σ m α

Lift the m monad into the EStateT ε σ m monad transformer.

Equations
• = do let ax pure ()
Instances For
instance Lake.EStateT.instMonadLiftOfMonad {m : Type u → Type u_1} {ε : Type u} {σ : Type u} [] :
Equations
@[inline]
def Lake.EStateT.pure {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Pure m] (a : α) :
Lake.EStateT ε σ m α

The pure operation of the EStateT monad transformer.

Equations
Instances For
instance Lake.EStateT.instPure {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Pure m] :
Pure (Lake.EStateT ε σ m)
Equations
• Lake.EStateT.instPure = { pure := fun {α : Type u_1} => Lake.EStateT.pure }
@[inline]
def Lake.EStateT.map {ε : Type u} {σ : Type v} {α : Type w} {β : Type w} {m : Type (max (max u v) w) → Type u_1} [] (f : αβ) (x : Lake.EStateT ε σ m α) :
Lake.EStateT ε σ m β

The map operation of the EStateT monad transformer.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance Lake.EStateT.instFunctor {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [] :
Equations
• Lake.EStateT.instFunctor = { map := fun {α β : Type u_1} => Lake.EStateT.map, mapConst := fun {α β : Type u_1} => Lake.EStateT.map }
@[inline]
def Lake.EStateT.bind {ε : Type u} {σ : Type v} {α : Type w} {β : Type w} {m : Type (max (max u v) w) → Type u_1} [] (x : Lake.EStateT ε σ m α) (f : αLake.EStateT ε σ m β) :
Lake.EStateT ε σ m β

The bind operation of the EStateT monad transformer.

Equations
• x.bind f s = do let __do_liftx s match __do_lift with | => f a s | => pure ()
Instances For
@[inline]
def Lake.EStateT.seqRight {ε : Type u} {σ : Type v} {α : Type w} {β : Type w} {m : Type (max (max u v) w) → Type u_1} [] (x : Lake.EStateT ε σ m α) (y : UnitLake.EStateT ε σ m β) :
Lake.EStateT ε σ m β

The seqRight operation of the EStateT monad transformer.

Equations
• x.seqRight y s = do let __do_liftx s match __do_lift with | => y () s | => pure ()
Instances For
@[always_inline]
instance Lake.EStateT.instMonad {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [] :
Equations
@[inline]
def Lake.EStateT.set {ε : Type u} {σ : Type v} {m : Type (max (max u v) w) → Type u_1} [Pure m] (s : σ) :

The set operation of the EStateT monad.

Equations
Instances For
@[inline]
def Lake.EStateT.get {ε : Type u} {σ : Type v} {m : Type (max u v) → Type u_1} [Pure m] :
Lake.EStateT ε σ m σ

The get operation of the EStateT monad.

Equations
Instances For
@[inline]
def Lake.EStateT.modifyGet {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Pure m] (f : σα × σ) :
Lake.EStateT ε σ m α

The modifyGet operation of the EStateT monad transformer.

Equations
• = match f s with | (a, s) => pure ()
Instances For
instance Lake.EStateT.instMonadStateOfOfPure {ε : Type u} {σ : Type v} {m : Type (max u v) → Type u_1} [Pure m] :
Equations
• Lake.EStateT.instMonadStateOfOfPure = { get := Lake.EStateT.get, set := Lake.EStateT.set, modifyGet := fun {α : Type v} => Lake.EStateT.modifyGet }
@[inline]
def Lake.EStateT.throw {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Pure m] (e : ε) :
Lake.EStateT ε σ m α

The throw operation of the EStateT monad transformer.

Equations
Instances For
@[inline]
def Lake.EStateT.tryCatch {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [] (x : Lake.EStateT ε σ m α) (handle : εLake.EStateT ε σ m α) :
Lake.EStateT ε σ m α
Equations
• x.tryCatch handle s = do let __do_liftx s match __do_lift with | => handle e s | ok => pure ok
Instances For
instance Lake.EStateT.instMonadExceptOfOfMonad {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [] :
Equations
• Lake.EStateT.instMonadExceptOfOfMonad = { throw := fun {α : Type u_1} => Lake.EStateT.throw, tryCatch := fun {α : Type u_1} => Lake.EStateT.tryCatch }
@[inline]
def Lake.EStateT.orElse {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [] (x₁ : Lake.EStateT ε σ m α) (x₂ : UnitLake.EStateT ε σ m α) :
Lake.EStateT ε σ m α
Equations
• x₁.orElse x₂ s = do let __do_liftx₁ s match __do_lift with | => x₂ () s | ok => pure ok
Instances For
instance Lake.EStateT.instOrElseOfMonad {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [] :
OrElse (Lake.EStateT ε σ m α)
Equations
• Lake.EStateT.instOrElseOfMonad = { orElse := Lake.EStateT.orElse }
@[inline]
def Lake.EStateT.adaptExcept {ε : Type u} {ε' : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [] (f : εε') (x : Lake.EStateT ε σ m α) :
Lake.EStateT ε' σ m α

Map the exception type of a EStateT ε σ m α by a function f : ε → ε'.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[always_inline]
instance Lake.EStateT.instMonadFinallyOfMonad {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [] :
Equations
• One or more equations did not get rendered due to their size.