def Lean.Meta.mkProdN (ts : Array Expr) (u : Level) : MetaM Expr

Given types tᵢ, return the tuple type t₁ × t₂ × … × tₙ. For n = 0, return PUnit with the given level + 1.

def Lean.Meta.mkProdMkN (es : Array Expr) (u : Level) : MetaM (Expr × Expr)

Given expressions eᵢ, return the tuple (e₁, e₂, …, eₙ) and its type t₁ × t₂ × … × tₙ. For n = 0, return PUnit.unit with the given level + 1.

def Lean.Meta.getProdFields (tuple tupleTy : Expr) : MetaM (Expr × Expr × Expr × Expr)

Given a product (e₁, e₂) of type t₁ × t₂, return (e₁, t₁, e₂, t₂).