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

Execute the action x, then restore the initial state. Returns the state after x finished.

Equations

• Lean.withoutModifyingState' x = Lean.withoutModifyingState do let result ← x let finalState ← Lean.saveState pure (result, finalState)