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)
: