- 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)