Similar to `MonadState`

, but it retrieves/restores only the "backtrackable" part of the state

- saveState : m s
- restoreState : s → m Unit

## 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.

## Equations

- One or more equations did not get rendered due to their size.

## 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`

.

## Equations

- One or more equations did not get rendered due to their size.

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

## Equations

- One or more equations did not get rendered due to their size.

## 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 α

## Equations

- Lean.commitIfNoEx x = do let s_1 ← Lean.saveState tryCatch x fun (ex : ε) => do Lean.restoreState s_1 throw ex

## Instances For

def
Lean.withoutModifyingState
{m : Type → Type}
{s : Type}
{α : 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)

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

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

instance
Lean.instMonadBacktrackExceptT
{s : Type}
{m : Type → Type}
{ε : Type}
[Lean.MonadBacktrack s m]
[Monad m]
:

Lean.MonadBacktrack s (ExceptT ε m)

## Equations

- Lean.instMonadBacktrackExceptT = { saveState := ExceptT.lift Lean.saveState, restoreState := fun (s_1 : s) => ExceptT.lift (Lean.restoreState s_1) }