∀ {α : Type} [inst : Lean.Quote α] (xs : Array α) (i : ℕ) (args : Array Lean.Term),
  Lean.quoteArray.go✝ xs i args =
    if h : i < xs.size then Lean.quoteArray.go✝¹ xs (i + 1) (args.push (Lean.quote `term xs[i]))
    else Lean.Syntax.mkCApp (Lean.Name.mkStr2 "Array" (String.Internal.append "mkArray" (toString xs.size))) args