Documentation

Mathlib.Tactic.TypeStar

Support for Sort* and Type*. #

These elaborate as Sort u and Type u with a fresh implicit universe variable u.

source
def Lean.Elab.Term.mkFreshLevelName (usedLevelNames : List Name) (namePrefix : Name := `u) :
Name

Given a namePrefix ( `u by default), returns the first name out of namePrefix_1, namePrefix_2, ... which does not appear in usedLevelNames. Note mkFreshLevelName does not attempt to use namePrefix itself as a level name.

Equations
Instances For
    source
    def Lean.Elab.Term.mkFreshLevelParam (namePrefix : Name := `u) (insert : List Name → Name → List Name := fun (x : List Name) (head : Name) => head :: x) :
    TermElabM Level

    Creates a fresh Level parameter which does not appear in the current state's levelNames, and updates the state to include the new level parameter.

    By default, the new level parameter is of the form u_i and is included in the state as the most recent level parameter (at the front of the list).

    Supplying a namePrefix will cause the new level parameter to be of the form namePrefix_i, with i starting at 1.

    The new level name can be inserted at a custom position in the list of level names by providing a function insert : List Name → Name → List Name which will be called as insert currentLevelNames newLevelName. It is expected that the result will contain the new level name and still contain all current level names.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Elab.Term.«termSort*» :
      ParserDescr

      The syntax variable (X Y ... Z : Sort*) creates a new distinct implicit universe variable for each variable in the sequence.

      Equations
      Instances For
        source
        def Lean.Elab.Term.«termType*» :
        ParserDescr

        The syntax variable (X Y ... Z : Type*) creates a new distinct implicit universe variable > 0 for each variable in the sequence.

        Equations
        Instances For