Documentation

Aesop.RuleSet

The Aesop-specific parts of an Aesop rule set. A BaseRuleSet stores global Aesop rules, e.g. safe and unsafe rules. It does not store simp theorems for the builtin norm simp rule; these are instead stored in a simp extension.

Instances For
    Equations
    • One or more equations did not get rendered due to their size.

    A global Aesop rule set. When we tag a declaration with @[aesop], it is stored in one or more of these rule sets. Internally, a GlobalRuleSet is composed of a BaseRuleSet (stored in an Aesop rule set extension) plus a set of simp theorems (stored in a SimpExtension).

    Instances For
      Equations

      The rule set used by an Aesop tactic call. A local rule set is produced by combining several global rule sets and possibly adding or erasing some individual rules.

      Instances For
        theorem Aesop.LocalRuleSet.simpTheoremsArrayNonempty (self : Aesop.LocalRuleSet) :
        0 < self.simpTheoremsArray.size

        The simp theorems array must contain at least one SimpTheorems structure. When a simp theorem is added to a LocalRuleSet, it is stored in this first SimpTheorems structure.

        theorem Aesop.LocalRuleSet.simprocsArrayNonempty (self : Aesop.LocalRuleSet) :
        0 < self.simprocsArray.size

        The simprocs array must contain at least one Simprocs structure, for the same reason as above.

        @[always_inline]
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[always_inline]
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[always_inline]
            def Aesop.LocalRuleSet.onBaseM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (f : Aesop.BaseRuleSetm (Aesop.BaseRuleSet × α)) (rs : Aesop.LocalRuleSet) :
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            Instances For
                              Equations
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Equations
                                        Instances For
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[always_inline]
                                                  Equations
                                                  • rs.applicableNormalizationRules goal = rs.applicableNormalizationRulesWith goal fun (x : Aesop.NormRule) => true
                                                  Instances For
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[always_inline]
                                                      Equations
                                                      Instances For
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          @[always_inline]
                                                          Equations
                                                          Instances For
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[always_inline]
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For