instance EStateM.instToStringResult {ε σ α : Type u} [ToString ε] [ToString α] : ToString (Result ε σ α)

Equations

• One or more equations did not get rendered due to their size.

instance EStateM.instReprResult {ε σ α : Type u} [Repr ε] [Repr α] : Repr (Result ε σ α)

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def EStateM.orElse' {ε σ α δ : Type u} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (useFirstEx : Bool := true) : EStateM ε σ α

Alternative orElse operator that allows callers to select which exception should be used when both operations fail. The default is to use the first exception since the standard orElse uses the second.

Equations

• One or more equations did not get rendered due to their size.

@[always_inline]

instance EStateM.instMonadFinally {ε σ : Type u} : MonadFinally (EStateM ε σ)

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def EStateM.fromStateM {ε σ α : Type} (x : StateM σ α) : EStateM ε σ α

Converts a state monad action into a state monad action with exceptions.

The resulting action does not throw an exception.

Equations

• EStateM.fromStateM x s = match StateT.run x s with | (a, s') => EStateM.Result.ok a s'