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

Equations

• Lean.Meta.instInhabitedSimpCongrTheorem.default = { theoremName := default, funName := default, hypothesesPos := default, priority := default }

instance Lean.Meta.instInhabitedSimpCongrTheorem : Inhabited SimpCongrTheorem

Equations

• Lean.Meta.instInhabitedSimpCongrTheorem = { default := Lean.Meta.instInhabitedSimpCongrTheorem.default }

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

Equations

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

instance Lean.Meta.instReprSimpCongrTheorem : Repr SimpCongrTheorem

Equations

• Lean.Meta.instReprSimpCongrTheorem = { reprPrec := Lean.Meta.instReprSimpCongrTheorem.repr }

structure Lean.Meta.SimpCongrTheorems : Type

• lemmas : SMap Name (List SimpCongrTheorem)

instance Lean.Meta.instInhabitedSimpCongrTheorems : Inhabited SimpCongrTheorems

Equations

• Lean.Meta.instInhabitedSimpCongrTheorems = { default := Lean.Meta.instInhabitedSimpCongrTheorems.default }

def Lean.Meta.instInhabitedSimpCongrTheorems.default : SimpCongrTheorems

Equations

• Lean.Meta.instInhabitedSimpCongrTheorems.default = { lemmas := default }

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

Equations

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

instance Lean.Meta.instReprSimpCongrTheorems : Repr SimpCongrTheorems

Equations

• Lean.Meta.instReprSimpCongrTheorems = { reprPrec := Lean.Meta.instReprSimpCongrTheorems.repr }

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

Equations

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

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

Equations

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

opaque Lean.Meta.congrExtension : SimpleScopedEnvExtension SimpCongrTheorem SimpCongrTheorems

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

Equations

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

def Lean.Meta.addSimpCongrTheorem (declName : Name) (attrKind : AttributeKind) (prio : Nat) : 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 : CoreM SimpCongrTheorems

Equations

• Lean.Meta.getSimpCongrTheorems = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.congrExtension __do_lift)