Documentation

Batteries.Lean.MonadBacktrack

def Lean.withoutModifyingState' {m : TypeType} {s : Type} {α : Type} [Monad m] [Lean.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
Instances For