@[specialize #[]]

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

Instantiate level parameters

@[specialize #[]]

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

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

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

Equations

• e.instantiateLevelParams paramNames lvls = if (paramNames.isEmpty || lvls.isEmpty) = true then e else Lean.Expr.instantiateLevelParamsCore (Lean.Expr.getParamSubst✝ paramNames lvls) e

def Lean.Expr.instantiateLevelParamsNoCache (e : Lean.Expr) (paramNames : List Lean.Name) (lvls : List Lean.Level) : Lean.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 : Lean.Expr) (paramNames : Array Lean.Name) (lvls : Array Lean.Level) : Lean.Expr

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