structure Lean.Meta.SimpCongrTheorem : Type

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

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

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

instance Lean.Meta.instInhabitedSimpCongrTheorem : Inhabited Lean.Meta.SimpCongrTheorem

instance Lean.Meta.instReprSimpCongrTheorem : Repr Lean.Meta.SimpCongrTheorem

structure Lean.Meta.SimpCongrTheorems : Type

• lemmas : Lean.SMap Lake.Name (List Lean.Meta.SimpCongrTheorem)

instance Lean.Meta.instInhabitedSimpCongrTheorems : Inhabited Lean.Meta.SimpCongrTheorems

instance Lean.Meta.instReprSimpCongrTheorems : Repr Lean.Meta.SimpCongrTheorems

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

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

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

Equations

• Lean.Meta.addSimpCongrTheoremEntry.insert e [] = [e]
• Lean.Meta.addSimpCongrTheoremEntry.insert e (e' :: es) = if e.priority ≥ e'.priority then e :: e' :: es else e' :: Lean.Meta.addSimpCongrTheoremEntry.insert e es

opaque Lean.Meta.congrExtension : Lean.SimpleScopedEnvExtension Lean.Meta.SimpCongrTheorem Lean.Meta.SimpCongrTheorems

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

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

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

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

def Lean.Meta.getSimpCongrTheorems : Lean.MetaM Lean.Meta.SimpCongrTheorems