Additions to Lean.Elab.Term
#
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.