Documentation

Lean.Meta.Tactic.Grind.ExtAttr

Grind extensionality attribute to mark which [ext] theorems should be used.

@[reducible, inline]

Extensionality theorems that can be used by grind

Equations
    Instances For
      Equations
        Instances For
          def Lean.Meta.Grind.addExtAttr (declName : Name) (attrKind : AttributeKind) :
          Equations
            Instances For
              Equations
                Instances For
                  Equations
                    Instances For