Documentation

Lean.Meta.Tactic.Grind.ExtAttr

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

source
@[reducible, inline]
abbrev Lean.Meta.Grind.ExtTheorems :
Type

Extensionality theorems that can be used by grind

Equations
    Instances For
      source
      opaque Lean.Meta.Grind.extTheoremsExt :
      SimpleScopedEnvExtension Name ExtTheorems
      source
      def Lean.Meta.Grind.validateExtAttr (declName : Name) :
      CoreM Unit
      Equations
        Instances For
          source
          def Lean.Meta.Grind.addExtAttr (declName : Name) (attrKind : AttributeKind) :
          CoreM Unit
          Equations
            Instances For
              source
              def Lean.Meta.Grind.eraseExtAttr (declName : Name) :
              CoreM Unit
              Equations
                Instances For
                  source
                  def Lean.Meta.Grind.isExtTheorem (declName : Name) :
                  CoreM Bool
                  Equations
                    Instances For