Documentation

Lean.Meta.Tactic.Grind.Injective

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

Set of Injective theorems.

Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Meta.Grind.InjectiveTheoremsArray :
      Type

      A collections of sets of Injective theorems.

      Equations
        Instances For
          source
          def Lean.Meta.Grind.mkInjectiveTheorem (declName : Name) :
          MetaM InjectiveTheorem
          Equations
            Instances For
              source
              def Lean.Meta.Grind.Extension.addInjectiveAttr (ext : Extension) (declName : Name) (attrKind : AttributeKind) :
              MetaM Unit
              Equations
                Instances For