{m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadLiftT BaseIO m] →
        Lean.Core.Context →
          Lean.Environment →
            (Lean.Name → Lean.ConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) →
              ℕ →
                ℕ →
                  (_ : Lean.NameGenerator) ×'
                      (_ : Array (Task (Lean.Meta.LazyDiscrTree.InitResults α))) ×' (_ : ℕ) ×' (_ : ℕ) ×' ℕ →
                    m (Array (Task (Lean.Meta.LazyDiscrTree.InitResults α)))