Documentation

Lean.Util.InstantiateLevelParams

@[specialize #[]]

Instantiate level parameters

Instances For

    Instantiate universe level parameters names paramNames with lvls in e. If the two lists have different length, the smallest one is used.

    Instances For

      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

        Instantiate universe level parameters names paramNames with lvls in e. If the two arrays have different length, the smallest one is used.

        Instances For