Documentation

Lean.Util.MonadBacktrack

@[specialize]
def Lean.commitWhenSome? {m : TypeType} {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
@[specialize]
def Lean.commitWhen {m : TypeType} {s : outParam Type} {ε : outParam (Type u_1)} [inst : Monad m] [inst : Lean.MonadBacktrack s m] [inst : MonadExcept ε m] (x : m Bool) :
Equations
@[specialize]
def Lean.commitIfNoEx {m : TypeType} {s : outParam Type} {ε : outParam (Type u_1)} {α : Type} [inst : Monad m] [inst : Lean.MonadBacktrack s m] [inst : MonadExcept ε m] (x : m α) :
m α
Equations
@[specialize]
def Lean.withoutModifyingState {m : TypeType} {s : outParam Type} {α : Type} [inst : Monad m] [inst : MonadFinally m] [inst : Lean.MonadBacktrack s m] (x : m α) :
m α
Equations
@[specialize]
def Lean.observing? {m : TypeType} {s : outParam Type} {ε : outParam (Type u_1)} {α : Type} [inst : Monad m] [inst : Lean.MonadBacktrack s m] [inst : MonadExcept ε m] (x : m α) :
m (Option α)
Equations
instance Lean.instMonadBacktrackExceptT {s : outParam Type} {m : TypeType} {ε : Type} [inst : Lean.MonadBacktrack s m] [inst : Monad m] :
Equations