class Lean.MonadBacktrack (s : outParam Type) (m : Type → Type) : Type

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

• saveState : m s
• restoreState : s → m Unit

def Lean.commitWhenSome? {m : Type → Type} {s : Type} {ε : Type u_1} {α : Type} [Monad m] [MonadBacktrack s m] [MonadExcept ε m] (x? : m (Option α)) : m (Option α)

Execute x?, but backtrack state if result is none or an exception was thrown.

def Lean.commitWhenSomeNoEx? {m : Type → Type} {s : Type} {ε : Type u_1} {α : Type} [Monad m] [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.

def Lean.commitWhen {m : Type → Type} {s : Type} {ε : Type u_1} [Monad m] [MonadBacktrack s m] [MonadExcept ε m] (x : m Bool) : m Bool

def Lean.commitIfNoEx {m : Type → Type} {s : Type} {ε : Type u_1} {α : Type} [Monad m] [MonadBacktrack s m] [MonadExcept ε m] (x : m α) : m α

def Lean.withoutModifyingState {m : Type → Type} {s α : Type} [Monad m] [MonadFinally m] [MonadBacktrack s m] (x : m α) : m α

def Lean.observing? {m : Type → Type} {s : Type} {ε : Type u_1} {α : Type} [Monad m] [MonadBacktrack s m] [MonadExcept ε m] (x : m α) : m (Option α)

instance Lean.instMonadBacktrackExceptTOfMonad {s : Type} {m : Type → Type} {ε : Type} [MonadBacktrack s m] [Monad m] : MonadBacktrack s (ExceptT ε m)