- saveState : m s
- restoreState : s → m Unit
Similar to MonadState, but it retrieves/restores only the "backtrackable" part of the state
Instances
@[specialize #[]]
def
Lean.commitWhenSome?
{m : Type → Type}
{s : Type}
{ε : Type u_1}
{α : Type}
[inst : Monad m]
[inst : Lean.MonadBacktrack s m]
[inst : MonadExcept ε m]
(x? : m (Option α))
:
m (Option α)
Equations
- One or more equations did not get rendered due to their size.
@[specialize #[]]
def
Lean.commitWhen
{m : Type → Type}
{s : Type}
{ε : Type u_1}
[inst : Monad m]
[inst : Lean.MonadBacktrack s m]
[inst : MonadExcept ε m]
(x : m Bool)
:
m Bool
Equations
- One or more equations did not get rendered due to their size.
@[specialize #[]]
def
Lean.commitIfNoEx
{m : Type → Type}
{s : Type}
{ε : Type u_1}
{α : Type}
[inst : Monad m]
[inst : Lean.MonadBacktrack s m]
[inst : MonadExcept ε m]
(x : m α)
:
m α
Equations
- Lean.commitIfNoEx x = do let s ← Lean.saveState tryCatch x fun ex => do Lean.restoreState s throw ex
@[specialize #[]]
def
Lean.withoutModifyingState
{m : Type → Type}
{s : Type}
{α : Type}
[inst : Monad m]
[inst : MonadFinally m]
[inst : Lean.MonadBacktrack s m]
(x : m α)
:
m α
Equations
- Lean.withoutModifyingState x = do let s ← Lean.saveState tryFinally x (Lean.restoreState s)
@[specialize #[]]
def
Lean.observing?
{m : Type → Type}
{s : Type}
{ε : Type u_1}
{α : Type}
[inst : Monad m]
[inst : Lean.MonadBacktrack s m]
[inst : MonadExcept ε m]
(x : m α)
:
m (Option α)
Equations
- One or more equations did not get rendered due to their size.
instance
Lean.instMonadBacktrackExceptT
{s : Type}
{m : Type → Type}
{ε : Type}
[inst : Lean.MonadBacktrack s m]
[inst : Monad m]
:
Lean.MonadBacktrack s (ExceptT ε m)
Equations
- Lean.instMonadBacktrackExceptT = { saveState := ExceptT.lift Lean.saveState, restoreState := fun s => ExceptT.lift (Lean.restoreState s) }