{α : Type} →
  Lean.Core.Context →
    Lean.NameGenerator →
      Lean.Environment →
        (Lean.Name →
            Lean.ConstantInfo →
              Lean.MetaM (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))) →
          ℕ → ℕ → ℕ → BaseIO (Lean.Meta.RefinedDiscrTree.InitResults✝ α)