Documentation

Lean.Util.InstantiateLevelParams

source
@[specialize #[]]
def Lean.Expr.instantiateLevelParamsCore (s : Lake.Name → Option Lean.Level) (e : Lean.Expr) :
Lean.Expr

Instantiate level parameters

Instances For
    source
    @[specialize #[]]
    def Lean.Expr.instantiateLevelParamsCore.replaceFn (s : Lake.Name → Option Lean.Level) (e : Lean.Expr) :
    Option Lean.Expr
    Instances For
      source
      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.

      Instances For
        source
        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.)

        Instances For
          source
          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.

          Instances For