instance
EStateM.instToStringResult
{ε : Type u}
{σ : Type u}
{α : Type u}
[inst : ToString ε]
[inst : ToString α]
:
ToString (EStateM.Result ε σ α)
Equations
- EStateM.instToStringResult = { toString := fun x => match x with | EStateM.Result.ok a x => "ok: " ++ toString a | EStateM.Result.error e x => "error: " ++ toString e }
instance
EStateM.instReprResult
{ε : Type u}
{σ : Type u}
{α : Type u}
[inst : Repr ε]
[inst : Repr α]
:
Repr (EStateM.Result ε σ α)
Equations
- EStateM.instReprResult = { reprPrec := fun x x_1 => match x, x_1 with | EStateM.Result.error e x, prec => Repr.addAppParen (Std.Format.text "EStateM.Result.error " ++ reprArg e) prec | EStateM.Result.ok a x, prec => Repr.addAppParen (Std.Format.text "EStateM.Result.ok " ++ reprArg a) prec }
@[inline]
def
EStateM.orElse'
{ε : Type u}
{σ : Type u}
{α : Type u}
{δ : outParam (Type u)}
[inst : EStateM.Backtrackable δ σ]
(x₁ : EStateM ε σ α)
(x₂ : EStateM ε σ α)
(useFirstEx : optParam Bool true)
:
EStateM ε σ α
Equations
- EStateM.orElse' x₁ x₂ useFirstEx s = let d := EStateM.Backtrackable.save s; match x₁ s with | EStateM.Result.error e₁ s₁ => match x₂ (EStateM.Backtrackable.restore s₁ d) with | EStateM.Result.error e₂ s₂ => EStateM.Result.error (if useFirstEx = true then e₁ else e₂) s₂ | ok => ok | ok => ok
Equations
- EStateM.instMonadFinallyEStateM = { tryFinally' := fun {α β} x h s => let r := x s; match r with | EStateM.Result.ok a s => match h (some a) s with | EStateM.Result.ok b s => EStateM.Result.ok (a, b) s | EStateM.Result.error e s => EStateM.Result.error e s | EStateM.Result.error e₁ s => match h none s with | EStateM.Result.ok x s => EStateM.Result.error e₁ s | EStateM.Result.error e₂ s => EStateM.Result.error e₂ s }
@[inline]
Equations
- EStateM.fromStateM x s = match StateT.run x s with | (a, s') => EStateM.Result.ok a s'