Lean.Meta.Tactic.Simp.Attr

source

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.

source

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.

source

opaque Lean.Meta.simpExtension :

SimpExtension

source

opaque Lean.Meta.sevalSimpExtension :

SimpExtension

source

def Lean.Meta.getSimpTheorems :

CoreM SimpTheorems

Equations

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

source

def Lean.Meta.getSEvalTheorems :

CoreM SimpTheorems

Equations

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

source

def Lean.Meta.Simp.Context.mkDefault :

MetaM Context

Equations

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