structure Lean.Meta.SimpCongrTheorem : Type

Data for user-defined theorems marked with the congr attribute.

This type should be confused with CongrTheorem which represents different kinds of automatically generated congruence theorems. The simp tactic also uses some of them.

• theoremName : Name
• funName : Name
• hypothesesPos : Array Nat
• priority : Nat

def Lean.Meta.instInhabitedSimpCongrTheorem.default : SimpCongrTheorem

@[implicit_reducible]

instance Lean.Meta.instInhabitedSimpCongrTheorem : Inhabited SimpCongrTheorem

def Lean.Meta.instReprSimpCongrTheorem.repr : SimpCongrTheorem → Nat → Format

@[implicit_reducible]

instance Lean.Meta.instReprSimpCongrTheorem : Repr SimpCongrTheorem

structure Lean.Meta.SimpCongrTheorems : Type

• lemmas : SMap Name (List SimpCongrTheorem)

@[implicit_reducible]

instance Lean.Meta.instInhabitedSimpCongrTheorems : Inhabited SimpCongrTheorems

def Lean.Meta.instInhabitedSimpCongrTheorems.default : SimpCongrTheorems

def Lean.Meta.instReprSimpCongrTheorems.repr : SimpCongrTheorems → Nat → Format

@[implicit_reducible]

instance Lean.Meta.instReprSimpCongrTheorems : Repr SimpCongrTheorems

def Lean.Meta.SimpCongrTheorems.get (d : SimpCongrTheorems) (declName : Name) : List SimpCongrTheorem

def Lean.Meta.addSimpCongrTheoremEntry (d : SimpCongrTheorems) (e : SimpCongrTheorem) : SimpCongrTheorems

opaque Lean.Meta.congrExtension : SimpleScopedEnvExtension SimpCongrTheorem SimpCongrTheorems

def Lean.Meta.mkSimpCongrTheorem (declName : Name) (prio : Nat) : MetaM SimpCongrTheorem

def Lean.Meta.addSimpCongrTheorem (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit

def Lean.Meta.getSimpCongrTheorems : CoreM SimpCongrTheorems