Documentation

Lean.Util.InstantiateLevelParams

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

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

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