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 : Lean.Name
• funName : Lean.Name
• hypothesesPos : Array Nat
• priority : Nat

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

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

structure Lean.Meta.SimpCongrTheorems : Type

• lemmas : Lean.SMap Lean.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 : Lean.Name) : List Lean.Meta.SimpCongrTheorem

Equations

• d.get declName = match d.lemmas.find? declName with | none => [] | some cs => cs

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

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

def Lean.Meta.mkSimpCongrTheorem (declName : Lean.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

Equations

• Lean.Meta.mkSimpCongrTheorem.onlyMVarsAt t mvarSet = (Lean.Expr.find? (fun (e : Lean.Expr) => e.isMVar && !Lean.RBTree.contains mvarSet e.mvarId!) t).isNone

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

Equations

• Lean.Meta.addSimpCongrTheorem declName attrKind prio = do let lemma ← Lean.Meta.mkSimpCongrTheorem declName prio Lean.ScopedEnvExtension.add Lean.Meta.congrExtension lemma attrKind

def Lean.Meta.getSimpCongrTheorems : Lean.CoreM Lean.Meta.SimpCongrTheorems