Rewriting with rfl-theorems in Sym.dsimp

Sym.dsimp reuses the Sym.simp theorems, but only the ones proved by rfl, since a rewrite step must hold by definitional equality. Theorems with hypotheses are never applied: there is no discharger, and the instantiated hypotheses would have to be part of a proof term. Definitions are unfolded by unfold instead of their equational theorems, which are rarely rfl-theorems.

def Lean.Meta.Sym.DSimp.rewriteWith (thm : Simp.Theorem) (e : Expr) : DSimpM Result

Tries to rewrite e using thm.

Equations

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

def Lean.Meta.Sym.DSimp.rewrite (thms : Simp.Theorems) : DSimproc

Rewrites e using the first applicable theorem in thms. The fallback theorems (Theorem.fallback) are tried only when no other theorem rewrites e.

Equations

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

structure Lean.Meta.Sym.DSimp.Decls : Type

The rfl-theorems and the definitions to unfold contributed by Sym.dsimp parameters.

• thms : Simp.Theorems
• toUnfold : NameSet

def Lean.Meta.Sym.DSimp.Decls.add (decls : Decls) (declName : Name) : MetaM Decls

Adds the declaration declName to decls. A theorem must be proved by rfl. A definition is unfolded (see unfold) under the same conditions as in Meta.simp (Simp.unfoldEvenWithEqns), and contributes its equational theorems proved by rfl. See also Sym.Simp.getSimpTheoremNames.

Equations

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

def Lean.Meta.Sym.DSimp.Decls.ofNames (declNames : Array Name) : MetaM Decls

Equations

• Lean.Meta.Sym.DSimp.Decls.ofNames declNames = Array.foldlM Lean.Meta.Sym.DSimp.Decls.add { } declNames

def Lean.Meta.Sym.DSimp.Decls.toDSimproc (decls : Decls) : DSimproc

The dsimproc unfolding the definitions and rewriting with the theorems in decls.

Equations

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