Documentation

Lean.Meta.Tactic.Grind.Injective

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

Set of Injective theorems.

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

    A collections of sets of Injective theorems.

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