def Lean.Meta.Sym.instantiateMVarsS (e : Expr) : SymM Expr

Instantiates metavariables occurring in e, and returns a maximally shared term.

Equations

• Lean.Meta.Sym.instantiateMVarsS e = if e.hasMVar = true then do let __do_lift ← Lean.instantiateMVars e Lean.Meta.Sym.shareCommon __do_lift else pure e