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

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

Head-only variant of instantiateMVarsS: instantiates and reshares only when the head of e is a metavariable, otherwise returns e unchanged.

Equations

• Lean.Meta.Sym.instantiateMVarsIfMVarAppS e = if e.getAppFn.isMVar = true then Lean.Meta.Sym.instantiateMVarsS e else pure e