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

Instantiates metavariables and applies shareCommon, which maintains the SymM invariants enabled in the current configuration (see Sym.Config).

def Lean.Meta.Sym.preprocessMVar (mvarId : MVarId) : SymM MVarId

Instantiates assigned metavariables, applies shareCommon, and eliminates holes (aka none cells) in the local context.

def Lean.Expr.checkMaxShared (e : Expr) (msg : String := "") : Meta.Sym.SymM Unit

Debug helper: throws if any subexpression of e is not in the table of maximally shared terms.

def Lean.MVarId.checkMaxShared (mvarId : MVarId) (msg : String := "") : Meta.Sym.SymM Unit

Debug helper: throws if any subexpression of the goal's target type is not in the table of maximally shared.

def Lean.Meta.Sym.normalizeLevels (e : Expr) : CoreM Expr

Normalizes universe levels in constants and sorts.