Documentation

Lean.Util.InstantiateLevelParams

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

Instantiate level parameters

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