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

Equations

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

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

Equations

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

@[inline]

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

Alternative orElse operator that allows to select which exception should be used. 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 ε σ α

Equations

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