Documentation

Mathlib.Lean.Elab.Term

Additions to Lean.Elab.Term #

source
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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For