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.

Equations

• Lean.Meta.Sym.withLocalDeclS name bi type k = Lean.Meta.withLocalDecl name bi type fun (x : Lean.Expr) => do let __do_lift ← liftM (Lean.Meta.Sym.Internal.mkFVarS x.fvarId!) k __do_lift

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.

Equations

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

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.