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.
Instances For
- lemmas : Lean.SMap Lake.Name (List Lean.Meta.SimpCongrTheorem)
Instances For
Instances For
def
Lean.Meta.addSimpCongrTheoremEntry
(d : Lean.Meta.SimpCongrTheorems)
(e : Lean.Meta.SimpCongrTheorem)
:
Instances For
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
Instances For
Instances For
Return true if t contains a metavariable that is not in mvarSet
Instances For
def
Lean.Meta.addSimpCongrTheorem
(declName : Lake.Name)
(attrKind : Lean.AttributeKind)
(prio : Nat)
: