- saveState : m s
- restoreState : s → m Unit
@[specialize]
def
Lean.commitWhenSome?
{m : Type → Type}
{s : outParam Type}
{ε : outParam (Type u_1)}
{α : Type}
[inst : Monad m]
[inst : Lean.MonadBacktrack s m]
[inst : MonadExcept ε m]
(x? : m (Option α))
:
m (Option α)
Equations
- Lean.commitWhenSome? x? = do let s ← Lean.saveState tryCatch (do let a ← x? match a with | some a => pure (some a) | none => do Lean.restoreState s pure none) fun ex => do Lean.restoreState s throw ex
@[specialize]
def
Lean.commitWhen
{m : Type → Type}
{s : outParam Type}
{ε : outParam (Type u_1)}
[inst : Monad m]
[inst : Lean.MonadBacktrack s m]
[inst : MonadExcept ε m]
(x : m Bool)
:
m Bool
Equations
- Lean.commitWhen x = do let s ← Lean.saveState tryCatch (do let a ← x match a with | true => pure true | false => do Lean.restoreState s pure false) fun ex => do Lean.restoreState s throw ex
@[specialize]
def
Lean.commitIfNoEx
{m : Type → Type}
{s : outParam Type}
{ε : outParam (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 : outParam 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 : outParam Type}
{ε : outParam (Type u_1)}
{α : Type}
[inst : Monad m]
[inst : Lean.MonadBacktrack s m]
[inst : MonadExcept ε m]
(x : m α)
:
m (Option α)
Equations
- Lean.observing? x = do let s ← Lean.saveState let r ← tryCatch (do let y ← x pure (DoResultPR.pure y PUnit.unit)) fun x => do Lean.restoreState s pure (DoResultPR.return none PUnit.unit) match r with | DoResultPR.pure a u => let x := u; pure (some a) | DoResultPR.return b u => let x := u; pure b
instance
Lean.instMonadBacktrackExceptT
{s : outParam 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) }