Additions to Lean.Elab.Term

def Lean.Elab.Term.elabPattern (patt : Term) (expectedType? : Option Expr) : TermElabM Expr

Fully elaborates the term patt, allowing typeclass inference failure, but while setting errToSorry to false. Typeclass failures result in plain metavariables. Instantiates all assigned metavariables.

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.

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.