@[inline, reducible]

abbrev Lake.EStateT (ε : Type u) (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v)

An exception plus state monad transformer (ι.e., ExceptT + StateT).

Equations

• Lake.EStateT ε σ m = ExceptT ε (StateT σ m)

@[inline]

def Lake.EStateT.run {ε : Type u} {σ : Type u} {m : Type u → Type v} {α : Type u} (init : σ) (self : Lake.EStateT ε σ m α) : m (Except ε α × σ)

Equations

• Lake.EStateT.run init self = StateT.run (ExceptT.run self) init

@[inline]

def Lake.EStateT.run' {ε : Type u} {σ : Type u} {m : Type u → Type v} {α : Type u} [Functor m] (init : σ) (self : Lake.EStateT ε σ m α) : m (Except ε α)

Equations

• Lake.EStateT.run' init self = StateT.run' (ExceptT.run self) init