- saveState : m s✝
- restoreState : s✝ → m Unit
Similar to MonadState, but it retrieves/restores only the "backtrackable" part of the state
Instances
def
Lean.commitWhenSome?
{m : Type → Type}
{s : Type}
{ε : Type u_1}
{α : Type}
[Monad m]
[Lean.MonadBacktrack s m]
[MonadExcept ε m]
(x? : m (Option α))
:
m (Option α)
Execute x?, but backtrack state if result is none or an exception was thrown.
Instances For
def
Lean.commitWhenSomeNoEx?
{m : Type → Type}
{s : Type}
{ε : Type u_1}
{α : Type}
[Monad m]
[Lean.MonadBacktrack s m]
[MonadExcept ε m]
(x? : m (Option α))
:
m (Option α)
Execute x?, but backtrack state if result is none or an exception was thrown.
If an exception is thrown, none is returned.
That is, this function is similar to commitWhenSome?, but swallows the exception and returns none.
Instances For
def
Lean.commitWhen
{m : Type → Type}
{s : Type}
{ε : Type u_1}
[Monad m]
[Lean.MonadBacktrack s m]
[MonadExcept ε m]
(x : m Bool)
:
m Bool
Instances For
def
Lean.commitIfNoEx
{m : Type → Type}
{s : Type}
{ε : Type u_1}
{α : Type}
[Monad m]
[Lean.MonadBacktrack s m]
[MonadExcept ε m]
(x : m α)
:
m α
Instances For
def
Lean.withoutModifyingState
{m : Type → Type}
{s : Type}
{α : Type}
[Monad m]
[MonadFinally m]
[Lean.MonadBacktrack s m]
(x : m α)
:
m α
Instances For
def
Lean.observing?
{m : Type → Type}
{s : Type}
{ε : Type u_1}
{α : Type}
[Monad m]
[Lean.MonadBacktrack s m]
[MonadExcept ε m]
(x : m α)
:
m (Option α)
Instances For
instance
Lean.instMonadBacktrackExceptT
{s : Type}
{m : Type → Type}
{ε : Type}
[Lean.MonadBacktrack s m]
[Monad m]
:
Lean.MonadBacktrack s (ExceptT ε m)