Documentation

Lean.Meta.Tactic.Simp.SimpCongrTheorems

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
    Equations
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.

    Return true if t contains a metavariable that is not in mvarSet

    Equations
    Equations