@[specialize #[]]

def Lean.Expr.instantiateLevelParamsCore (s : Name → Option Level) (e : Expr) : Expr

Instantiate level parameters

@[specialize #[]]

def Lean.Expr.instantiateLevelParamsCore.replaceFn (s : Name → Option Level) (e : Expr) : Option Expr

def Lean.Expr.instantiateLevelParams (e : Expr) (paramNames : List Name) (lvls : List Level) : Expr

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

def Lean.Expr.instantiateLevelParamsNoCache (e : Expr) (paramNames : List Name) (lvls : List Level) : Expr

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.)

def Lean.Expr.instantiateLevelParamsArray (e : Expr) (paramNames : Array Name) (lvls : Array Level) : Expr

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