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

instance Lean.Meta.instInhabitedSimpCongrTheorem : Inhabited SimpCongrTheorem

instance Lean.Meta.instReprSimpCongrTheorem : Repr SimpCongrTheorem

structure Lean.Meta.SimpCongrTheorems : Type

• lemmas : SMap Name (List SimpCongrTheorem)

instance Lean.Meta.instInhabitedSimpCongrTheorems : Inhabited SimpCongrTheorems

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

def Lean.Meta.addSimpCongrTheoremEntry.insert (e : SimpCongrTheorem) : List SimpCongrTheorem → List SimpCongrTheorem

opaque Lean.Meta.congrExtension : SimpleScopedEnvExtension SimpCongrTheorem SimpCongrTheorems

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

def Lean.Meta.mkSimpCongrTheorem.onlyMVarsAt (t : Expr) (mvarSet : MVarIdSet) : Bool

Return true if t contains a metavariable that is not in mvarSet

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

def Lean.Meta.getSimpCongrTheorems : CoreM SimpCongrTheorems