@[specialize #[]]
Instantiate level parameters
Instances For
@[specialize #[]]
def
Lean.Expr.instantiateLevelParamsCore.replaceFn
(s : Lake.Name → Option Lean.Level)
(e : Lean.Expr)
:
Instances For
def
Lean.Expr.instantiateLevelParams
(e : Lean.Expr)
(paramNames : List Lake.Name)
(lvls : List Lean.Level)
:
Instantiate universe level parameters names paramNames with lvls in e.
If the two lists have different length, the smallest one is used.
Instances For
def
Lean.Expr.instantiateLevelParamsNoCache
(e : Lean.Expr)
(paramNames : List Lake.Name)
(lvls : List Lean.Level)
:
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.)
Instances For
def
Lean.Expr.instantiateLevelParamsArray
(e : Lean.Expr)
(paramNames : Array Lake.Name)
(lvls : Array Lean.Level)
:
Instantiate universe level parameters names paramNames with lvls in e.
If the two arrays have different length, the smallest one is used.