Documentation

Lake.Util.EStateT

@[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
@[inline]
def Lake.EStateT.run {ε : Type u} {σ : Type u} {m : Type u → Type v} {α : Type u} (init : σ) (self : Lake.EStateT ε σ m α) :
m (Except ε α × σ)
Equations
@[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