Documentation

Aesop.Frontend.Attribute

source
def Aesop.Frontend.Parser.Aesop.attr_rules.quot :
Lean.ParserDescr
Equations
    Instances For
      source
      def Lean.Parser.Category.Aesop.attr_rules :
      Category
      Equations
        Instances For
          source
          def Aesop.Frontend.Parser.attr_rules_ :
          Lean.ParserDescr
          Equations
            Instances For
              source
              def Aesop.Frontend.Parser.«attr_rules[_]» :
              Lean.ParserDescr
              Equations
                Instances For
                  source
                  def Aesop.Frontend.Parser.aesop :
                  Lean.ParserDescr
                  Equations
                    Instances For
                      source
                      structure Aesop.Frontend.AttrConfig :
                      Type
                      Instances For
                        source
                        instance Aesop.Frontend.instInhabitedAttrConfig :
                        Inhabited AttrConfig
                        Equations
                          source
                          def Aesop.Frontend.AttrConfig.elab (stx : Lean.Syntax) :
                          Lean.Elab.TermElabM AttrConfig
                          Equations
                            Instances For