@[specialize #[]]

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

Instantiate level parameters

Equations

• Lean.Expr.instantiateLevelParamsCore s e = Lean.Expr.replace (Lean.Expr.instantiateLevelParamsCore.replaceFn s) e

@[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.

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

Equations

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

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.

Equations

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