Documentation

Lean.Meta.Tactic.Grind.Attr

source
opaque Lean.Meta.Grind.normExt :
SimpExtension
source
inductive Lean.Meta.Grind.AttrKind :
Type
Instances For
    source
    def Lean.Meta.Grind.getAttrKindCore (stx : Syntax) :
    CoreM AttrKind

    Return theorem kind for stx of the form Attr.grindThmMod

    Instances For
      source
      def Lean.Meta.Grind.getAttrKindFromOpt (stx : Syntax) :
      CoreM AttrKind

      Return theorem kind for stx of the form (Attr.grindMod)?

      Instances For
        source
        def Lean.Meta.Grind.throwInvalidUsrModifier {α : Type} :
        CoreM α
        Instances For
          source
          @[reducible, inline]
          abbrev Lean.Meta.Grind.ExtensionMap :
          Type
          Instances For
            source
            opaque Lean.Meta.Grind.extensionMapRef :
            IO.Ref ExtensionMap
            source
            def Lean.Meta.Grind.getExtension? (attrName : Name) :
            CoreM (Option Extension)
            Instances For
              source
              def Lean.Meta.Grind.registerAttr (attrName : Name) (ref : Name := by exact decl_name%) :
              IO Extension
              Instances For
                source
                opaque Lean.Meta.Grind.grindExt :
                Extension
                source
                def Lean.Meta.Grind.isGlobalSplit (declName : Name) :
                CoreM Bool

                Returns true is declName is a builtin split or has been tagged with [grind] attribute.

                Instances For