Support for Sort* and Type*.

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

def «termSort*» : Lean.ParserDescr

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

Equations

• «termSort*» = Lean.ParserDescr.node `«termSort*» 1024 (Lean.ParserDescr.symbol "Sort*")

def «termType*» : Lean.ParserDescr

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

Equations

• «termType*» = Lean.ParserDescr.node `«termType*» 1024 (Lean.ParserDescr.symbol "Type*")