HepLean Documentation

Mathlib.Lean.Elab.Term

Additions to Lean.Elab.Term #

source
def Lean.Elab.Term.elabPattern (patt : Lean.Term) (expectedType? : Option Lean.Expr) :
Lean.Elab.TermElabM Lean.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