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.

This is a universe-polymorphic version of EStateM.Result.

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

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

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

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

instance Lake.instInhabitedEResult {α : Type u_1} {σ : Type u_2} {ε : Type u_3} [Inhabited α] [Inhabited σ] : Inhabited (EResult ε σ α)

instance Lake.instInhabitedEResult_1 {ε : Type u_1} {σ : Type u_2} {α : Type u_3} [Inhabited ε] [Inhabited σ] : Inhabited (EResult ε σ α)

@[inline]

def Lake.EResult.state {ε : Type u_1} {σ : Type u_2} {α : Type u_3} : EResult ε σ α → σ

Extract the state σ from a EResult ε σ α.

@[inline]

def Lake.EResult.modifyState {σ : Type u_1} {σ' : Type u_2} {ε : Type u_3} {α : Type u_4} (f : σ → σ') : EResult ε σ α → EResult ε σ' α

@[inline]

def Lake.EResult.setState {σ' : Type u_1} {ε : Type u_2} {σ : Type u_3} {α : Type u_4} (s : σ') (r : EResult ε σ α) : EResult ε σ' α

@[inline]

def Lake.EResult.toProd {ε : Type u_1} {σ : Type u_2} {α : Type u_3} : EResult ε σ α → Except ε α × σ

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

@[inline]

def Lake.EResult.toProd? {ε : Type u_1} {σ : Type u_2} {α : Type u_3} : EResult ε σ α → Option α × σ

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

@[inline]

def Lake.EResult.result? {ε : Type u_1} {σ : Type u_2} {α : Type u_3} : EResult ε σ α → Option α

Extract the result α from a EResult ε σ α.

@[inline]

def Lake.EResult.error? {ε : Type u_1} {σ : Type u_2} {α : Type u_3} : EResult ε σ α → Option ε

Extract the error ε from a EResult ε σ α.

@[inline]

def Lake.EResult.toExcept {ε : Type u_1} {σ : Type u_2} {α : Type u_3} : EResult ε σ α → Except ε α

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

@[inline]

def Lake.EResult.map {α : Type u_1} {β : Type u_2} {ε : Type u_3} {σ : Type u_4} (f : α → β) : EResult ε σ α → EResult ε σ β

instance Lake.instFunctorEResult {ε : Type u_1} {σ : Type u_2} : Functor (EResult ε σ)

def Lake.EResult.toEStateMResult {ε σ α : Type u_1} : EResult ε σ α → EStateM.Result ε σ α

def Lake.EResult.ofEStateMResult {ε σ α : Type u_1} : EStateM.Result ε σ α → EResult ε σ α

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.

instance Lake.EStateT.instInhabitedOfPure {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Inhabited ε] [Pure m] : Inhabited (EStateT ε σ m α)

@[inline]

def Lake.EStateT.run {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max u v w) → Type u_1} (init : σ) (self : EStateT ε σ m α) : m (EResult ε σ α)

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

@[inline]

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

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

@[inline]

def Lake.EStateT.toStateT {m : Type u → Type u_1} {ε σ α : Type u} [Functor m] (x : EStateT ε σ m α) : StateT σ m (Except ε α)

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

@[inline]

def Lake.EStateT.toStateT? {m : Type u → Type u_1} {ε σ α : Type u} [Functor m] (x : EStateT ε σ m α) : StateT σ m (Option α)

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

@[inline]

def Lake.EStateT.run? {σ : Type v} {α : Type w} {m : Type (max v w) → Type u_1} {ε : Type (max v w)} [Functor m] (init : σ) (x : EStateT ε σ m α) : m (Option α × σ)

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

@[inline]

def Lake.EStateT.run?' {m : Type u → Type u_1} {ε σ α : Type u} [Functor m] (init : σ) (x : EStateT ε σ m α) : m (Option α)

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

@[inline]

def Lake.EStateT.catchExceptions {m : Type u → Type u_1} {ε σ α : Type u} [Monad m] (x : EStateT ε σ m α) (h : ε → StateT σ m α) : StateT σ m α

@[inline]

def Lake.EStateT.lift {m : Type u → Type u_1} {ε σ α : Type u} [Monad m] (x : m α) : EStateT ε σ m α

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

instance Lake.EStateT.instMonadLiftOfMonad {m : Type u → Type u_1} {ε σ : Type u} [Monad m] : MonadLift m (EStateT ε σ m)

@[inline]

def Lake.EStateT.pure {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Pure m] (a : α) : EStateT ε σ m α

The pure operation of the EStateT monad transformer.

instance Lake.EStateT.instPure {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Pure m] : Pure (EStateT ε σ m)

@[inline]

def Lake.EStateT.map {ε : Type u} {σ : Type v} {α β : Type w} {m : Type (max (max u v) w) → Type u_1} [Functor m] (f : α → β) (x : EStateT ε σ m α) : EStateT ε σ m β

The map operation of the EStateT monad transformer.

instance Lake.EStateT.instFunctor {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Functor m] : Functor (EStateT ε σ m)

@[inline]

def Lake.EStateT.bind {ε : Type u} {σ : Type v} {α β : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x : EStateT ε σ m α) (f : α → EStateT ε σ m β) : EStateT ε σ m β

The bind operation of the EStateT monad transformer.

@[inline]

def Lake.EStateT.seqRight {ε : Type u} {σ : Type v} {α β : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x : EStateT ε σ m α) (y : Unit → EStateT ε σ m β) : EStateT ε σ m β

The seqRight operation of the EStateT monad transformer.

@[always_inline]

instance Lake.EStateT.instMonad {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Monad m] : Monad (EStateT ε σ m)

@[inline]

def Lake.EStateT.set {ε : Type u} {σ : Type v} {m : Type (max (max u v) w) → Type u_1} [Pure m] (s : σ) : EStateT ε σ m PUnit

The set operation of the EStateT monad.

@[inline]

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

The get operation of the EStateT monad.

@[inline]

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

The modifyGet operation of the EStateT monad transformer.

instance Lake.EStateT.instMonadStateOfOfPure {ε : Type u} {σ : Type v} {m : Type (max u v) → Type u_1} [Pure m] : MonadStateOf σ (EStateT ε σ m)

@[inline]

def Lake.EStateT.throw {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Pure m] (e : ε) : EStateT ε σ m α

The throw operation of the EStateT monad transformer.

@[inline]

def Lake.EStateT.tryCatch {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x : EStateT ε σ m α) (handle : ε → EStateT ε σ m α) : EStateT ε σ m α

instance Lake.EStateT.instMonadExceptOfOfMonad {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Monad m] : MonadExceptOf ε (EStateT ε σ m)

@[inline]

def Lake.EStateT.orElse {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x₁ : EStateT ε σ m α) (x₂ : Unit → EStateT ε σ m α) : EStateT ε σ m α

instance Lake.EStateT.instOrElseOfMonad {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] : OrElse (EStateT ε σ m α)

@[inline]

def Lake.EStateT.adaptExcept {ε ε' : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Functor m] (f : ε → ε') (x : EStateT ε σ m α) : EStateT ε' σ m α

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

@[always_inline]

instance Lake.EStateT.instMonadFinallyOfMonad {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Monad m] : MonadFinally (EStateT ε σ m)

def Lake.EStateT.ofEStateM {ε σ α : Type u_1} (f : EStateM ε σ α) : EStateT ε σ Id α

EStateM is analogous to Lake.EStateT with m := Id.

def Lake.EStateT.toEStateM {ε σ α : Type u_1} (f : EStateT ε σ Id α) : EStateM ε σ α

Lake.EStateT with m := Id and all the types in the same universe is analogous to EStateM.