def Lean.Meta.addDeclToUnfold (ext : SimpExtension) (declName : Name) (post inv : Bool) (prio : Nat) (attrKind : AttributeKind) : MetaM Bool

Marks declName to be unfolded in the given SimpExtension.

Equations

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

def Lean.Meta.mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension) (ref : Name := by exact decl_name%) : IO Unit

Equations

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

def Lean.Meta.registerSimpAttr (attrName : Name) (attrDescr : String) (ref : Name := by exact decl_name%) : IO SimpExtension

Registers the given name as a custom simp set. Applying the name as an attribute to a name adds it to the simp set, and using the name as a parameter to the simp tactic causes simp to use the included lemmas.

Custom simp sets must be registered during initialization.

The description should be a short, singular noun phrase that describes the contents of the custom simp set.

Equations

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

opaque Lean.Meta.simpExtension : SimpExtension

opaque Lean.Meta.sevalSimpExtension : SimpExtension

def Lean.Meta.getSimpTheorems : CoreM SimpTheorems

Equations

• Lean.Meta.getSimpTheorems = Lean.Meta.simpExtension.getTheorems

def Lean.Meta.getSEvalTheorems : CoreM SimpTheorems

Equations

• Lean.Meta.getSEvalTheorems = Lean.Meta.sevalSimpExtension.getTheorems

def Lean.Meta.Simp.Context.mkDefault : MetaM Context

Equations

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