HepLean Documentation

Aesop.RuleSet.Name

source
@[reducible, inline]
abbrev Aesop.RuleSetName :
Type
Equations
Instances For
    source
    def Aesop.defaultRuleSetName :
    Aesop.RuleSetName
    Equations
    Instances For
      source
      def Aesop.builtinRuleSetName :
      Aesop.RuleSetName
      Equations
      Instances For
        source
        def Aesop.localRuleSetName :
        Aesop.RuleSetName
        Equations
        Instances For
          source
          def Aesop.builtinRuleSetNames :
          Array Aesop.RuleSetName
          Equations
          Instances For
            source
            def Aesop.RuleSetName.isReserved (n : Aesop.RuleSetName) :
            Bool
            Equations
            Instances For