@[specialize #[]]

def Lean.Expr.instantiateLevelParamsCore (s : Lake.Name → Option Lean.Level) (e : Lean.Expr) : Lean.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 : Lake.Name → Option Lean.Level) (e : Lean.Expr) : Option Lean.Expr

def Lean.Expr.instantiateLevelParams (e : Lean.Expr) (paramNames : List Lake.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 Lake.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.)

Equations

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

def Lean.Expr.instantiateLevelParamsArray (e : Lean.Expr) (paramNames : Array Lake.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.

Equations

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