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

Equations

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

instance Lean.Meta.instReprSimpCongrTheorem : Repr SimpCongrTheorem

Equations

• Lean.Meta.instReprSimpCongrTheorem = { reprPrec := Lean.Meta.reprSimpCongrTheorem✝ }

structure Lean.Meta.SimpCongrTheorems : Type

• lemmas : SMap Name (List SimpCongrTheorem)

instance Lean.Meta.instInhabitedSimpCongrTheorems : Inhabited SimpCongrTheorems

Equations

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

instance Lean.Meta.instReprSimpCongrTheorems : Repr SimpCongrTheorems

Equations

• Lean.Meta.instReprSimpCongrTheorems = { reprPrec := Lean.Meta.reprSimpCongrTheorems✝ }

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.

def Lean.Meta.addSimpCongrTheoremEntry.insert (e : SimpCongrTheorem) : List SimpCongrTheorem → List 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 : 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.mkSimpCongrTheorem.onlyMVarsAt (t : Expr) (mvarSet : 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 : 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)