def Lean.Meta.Sym.unfoldReducibleStep (e : Expr) : MetaM TransformStep

Auxiliary function for implementing unfoldReducible and unfoldReducibleSimproc. Performs a single step.

def Lean.Meta.Sym.unfoldReducible (e : Expr) : MetaM Expr

Unfolds all reducible declarations occurring in e. This is meant as a preprocessing step. It does not guarantee maximally shared terms

def Lean.Meta.Sym.foldProjs (e : Expr) : MetaM Expr

Converts nested Expr.projs into projection applications if possible. The structural simplifier and pattern matcher do not handle kernel projection terms; this preprocessing step folds them into projection function applications.

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.