def Lean.Meta.Sym.withLocalDeclS {n : Type → Type u_1} {α : Type} [Monad n] [MonadControlT MetaM n] [MonadLiftT SymM n] (name : Name) (bi : BinderInfo) (type : Expr) (k : Expr → n α) : n α

Similar to withLocalDecl, but the free variable passed to k is registered in the SymM share set. Use it when the free variable is substituted into maximally shared terms, e.g. via instantiateRevS.

def Lean.Meta.Sym.withLetDeclS {n : Type → Type u_1} {α : Type} [Monad n] [MonadControlT MetaM n] [MonadLiftT SymM n] (name : Name) (type val : Expr) (k : Expr → n α) (nondep : Bool := false) : n α

withLetDecl variant that registers the free variable in the share set. See withLocalDeclS.

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.