Similar to MonadState, but it retrieves/restores only the "backtrackable" part of the state
- saveState : m s
- restoreState : s → m Unit
Instances
- Aesop.instMonadBacktrackSavedStateNormM
- Lean.Elab.Tactic.instMonadBacktrackSavedStateTacticM
- Lean.Elab.Term.instMonadBacktrackSavedStateTermElabM
- Lean.Meta.ElimEmptyInductive.instMonadBacktrackSavedStateM
- Lean.Meta.instMonadBacktrackSavedStateMetaM
- Lean.instMonadBacktrackExceptTOfMonad
- instMonadBacktrackUnitId_batteries
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.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
def
Lean.commitWhen
{m : Type → Type}
{s : Type}
{ε : Type u_1}
[Monad m]
[Lean.MonadBacktrack s m]
[MonadExcept ε m]
(x : m Bool)
:
m Bool
Equations
- One or more equations did not get rendered due to their size.
def
Lean.commitIfNoEx
{m : Type → Type}
{s : Type}
{ε : Type u_1}
{α : Type}
[Monad m]
[Lean.MonadBacktrack s m]
[MonadExcept ε m]
(x : m α)
:
m α
Equations
- Lean.commitIfNoEx x = do let s_1 ← Lean.saveState tryCatch x fun (ex : ε) => do Lean.restoreState s_1 throw ex
def
Lean.withoutModifyingState
{m : Type → Type}
{s α : Type}
[Monad m]
[MonadFinally m]
[Lean.MonadBacktrack s m]
(x : m α)
:
m α
Equations
- Lean.withoutModifyingState x = do let s_1 ← Lean.saveState tryFinally x (Lean.restoreState s_1)
def
Lean.observing?
{m : Type → Type}
{s : Type}
{ε : Type u_1}
{α : Type}
[Monad m]
[Lean.MonadBacktrack s m]
[MonadExcept ε m]
(x : m α)
:
m (Option α)
Equations
- One or more equations did not get rendered due to their size.
instance
Lean.instMonadBacktrackExceptTOfMonad
{s : Type}
{m : Type → Type}
{ε : Type}
[Lean.MonadBacktrack s m]
[Monad m]
:
Lean.MonadBacktrack s (ExceptT ε m)
Equations
- Lean.instMonadBacktrackExceptTOfMonad = { saveState := ExceptT.lift Lean.saveState, restoreState := fun (s_1 : s) => ExceptT.lift (Lean.restoreState s_1) }