def Lean.Meta.repeat'Core {m : Type → Type} {ε : Type u_1} {s : Type} [Monad m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m] (f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters : Nat := 100000) : m (Bool × List MVarId)

Implementation of repeat' and repeat1'.

repeat'Core f runs f on all of the goals to produce a new list of goals, then runs f again on all of those goals, and repeats until f fails on all remaining goals, or until maxIters total calls to f have occurred.

Returns a boolean indicating whether f succeeded at least once, and all the remaining goals (i.e. those on which f failed).

def Lean.Meta.repeat' {m : Type → Type} {ε : Type u_1} {s : Type} [Monad m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m] (f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters : Nat := 100000) : m (List MVarId)

repeat' f runs f on all of the goals to produce a new list of goals, then runs f again on all of those goals, and repeats until f fails on all remaining goals, or until maxIters total calls to f have occurred. Always succeeds (returning the original goals if f fails on all of them).

def Lean.Meta.repeat1' {m : Type → Type} {ε : Type u_1} {s : Type} [Monad m] [MonadError m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m] (f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters : Nat := 100000) : m (List MVarId)

repeat1' f runs f on all of the goals to produce a new list of goals, then runs f again on all of those goals, and repeats until f fails on all remaining goals, or until maxIters total calls to f have occurred. Fails if f does not succeed at least once.