# Documentation

Lean.Util.InstantiateLevelParams

@[specialize #[]]

Instantiate level parameters

Equations
@[specialize #[]]
Equations
• One or more equations did not get rendered due to their size.
def Lean.Expr.instantiateLevelParams (e : Lean.Expr) (paramNames : ) (lvls : ) :

Instantiate universe level parameters names paramNames with lvls in e. If the two lists have different length, the smallest one is used.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Expr.instantiateLevelParamsNoCache (e : Lean.Expr) (paramNames : ) (lvls : ) :

Instantiate universe level parameters names paramNames with lvls in e. If the two lists have different length, the smallest one is used. (Does not preserve expression sharing.)

Equations
• One or more equations did not get rendered due to their size.
def Lean.Expr.instantiateLevelParamsArray (e : Lean.Expr) (paramNames : ) (lvls : ) :

Instantiate universe level parameters names paramNames with lvls in e. If the two arrays have different length, the smallest one is used.

Equations
• One or more equations did not get rendered due to their size.