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

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

Equations

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

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

Equations

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

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.

Equations

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

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

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

Equations

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

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.

Equations

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

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.

Equations

• mvarId.checkMaxShared msg = do let __do_lift ← liftM mvarId.getDecl __do_lift.type.checkMaxShared msg

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

Normalizes universe levels in constants and sorts.

Equations

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