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