Documentation

Lean.Meta.Tactic.Simp.SimpCongrTheorems

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.

Instances For
    Equations
    Equations
    • d.get declName = match d.lemmas.find? declName with | none => [] | some cs => cs
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

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

          Equations
          Instances For
            Equations
            Instances For