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).

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.