elabTermWithoutNewMVars

def elabTermWithoutNewMVars (tactic : Lean.Name) (t : Lean.Term) : Lean.Elab.Tactic.TacticM Lean.Expr

Elaborates a term with errToSorry = false and ensuring it has no metavariables.