∀ {m : Type → Type u_1} {α : Type} [inst : MonadControlT Lean.Elab.Tactic.Do.VCGenM m] (xs : Array Lean.Expr) (k : m α)
  (runInBase : {β : Type} → m β → Lean.Elab.Tactic.Do.VCGenM (stM Lean.Elab.Tactic.Do.VCGenM m β)) (i : ℕ),
  Lean.Elab.Tactic.Do.withLocalSpecs.loop✝ xs k runInBase i =
    if h : i < xs.size then
      have x := xs[i];
      tryCatch
        (do
          let thm ← liftM (Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremFromLocal x.fvarId! 100)
          have cls : Lean.Name := `Elab.Tactic.Do.vcgen
          let __do_lift ← Lean.isTracingEnabledFor cls
          have __do_jp : Unit → Lean.Elab.Tactic.Do.VCGenM (stM Lean.Elab.Tactic.Do.VCGenM m α) := fun y =>
            withReader
              (fun ctx =>
                { config := ctx.config, specThms := ctx.specThms.insert thm, simpCtx := ctx.simpCtx,
                  simprocs := ctx.simprocs, jps := ctx.jps, initialCtxSize := ctx.initialCtxSize })
              (Lean.Elab.Tactic.Do.withLocalSpecs.loop✝¹ xs k runInBase (i + 1))
          if __do_lift = true then do
              let y ← Lean.addTrace cls (Lean.toMessageData "adding " ++ Lean.toMessageData thm.proof)
              __do_jp y
            else do
              let y ← pure PUnit.unit
              __do_jp y)
        fun ex =>
        match ex with
        | Lean.Exception.internal id extra => throw ex
        | Lean.Exception.error ref msg => Lean.Elab.Tactic.Do.withLocalSpecs.loop✝² xs k runInBase (i + 1)
    else runInBase k