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.

Equations

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