def Lean.Meta.repeat'Core {m : Type → Type} {ε : Type u_1} {s : Type} [Monad m] [MonadExcept ε m] [Lean.MonadBacktrack s m] [Lean.MonadMCtx m] (f : Lean.MVarId → m (List Lean.MVarId)) (goals : List Lean.MVarId) (maxIters : optParam Nat 100000) : m (Bool × List Lean.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).

Equations

• One or more equations did not get rendered due to their size.

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

Auxiliary for repeat'Core. repeat'Core.go f maxIters progress goals stk acc evaluates to essentially acc.toList ++ repeat' f (goals::stk).join maxIters: that is, acc are goals we will not revisit, and (goals::stk).join is the accumulated todo list of subgoals.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.repeat'Core.go f x✝¹ x✝ [] [] x = pure (x✝, x)
• Lean.Meta.repeat'Core.go f x✝¹ x✝ [] (goals :: stk) x = Lean.Meta.repeat'Core.go f x✝¹ x✝ goals stk x

def Lean.Meta.repeat' {m : Type → Type} {ε : Type u_1} {s : Type} [Monad m] [MonadExcept ε m] [Lean.MonadBacktrack s m] [Lean.MonadMCtx m] (f : Lean.MVarId → m (List Lean.MVarId)) (goals : List Lean.MVarId) (maxIters : optParam Nat 100000) : m (List Lean.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).

Equations

• Lean.Meta.repeat' f goals maxIters = Lean.Meta.repeat'Core f goals maxIters <&> fun (x : Bool × List Lean.MVarId) => x.snd

def Lean.Meta.repeat1' {m : Type → Type} {ε : Type u_1} {s : Type} [Monad m] [Lean.MonadError m] [MonadExcept ε m] [Lean.MonadBacktrack s m] [Lean.MonadMCtx m] (f : Lean.MVarId → m (List Lean.MVarId)) (goals : List Lean.MVarId) (maxIters : optParam Nat 100000) : m (List Lean.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.

Equations

• One or more equations did not get rendered due to their size.