Documentation

Aesop.Tree.Data.ForwardRuleMatches

source
structure Aesop.ForwardRuleMatches :
Type

Sets of complete matches for norm/safe/unsafe rules.

Instances For
    source
    def Aesop.instInhabitedForwardRuleMatches.default :
    ForwardRuleMatches
    Instances For
      source
      @[implicit_reducible]
      instance Aesop.instInhabitedForwardRuleMatches :
      Inhabited ForwardRuleMatches
      source
      def Aesop.ForwardRuleMatches.empty :
      ForwardRuleMatches

      Empty ForwardRuleMatches.

      Instances For
        source
        @[implicit_reducible]
        instance Aesop.ForwardRuleMatches.instEmptyCollection :
        EmptyCollection ForwardRuleMatches
        source
        def Aesop.ForwardRuleMatches.insert (m : ForwardRuleMatch) (ms : ForwardRuleMatches) :
        ForwardRuleMatches

        Add a complete match.

        Instances For
          source
          def Aesop.ForwardRuleMatches.insertMany (ms : Array ForwardRuleMatch) (ms' : ForwardRuleMatches) :
          ForwardRuleMatches

          Add several complete matches.

          Instances For
            source
            def Aesop.ForwardRuleMatches.erase (m : ForwardRuleMatch) (ms : ForwardRuleMatches) :
            ForwardRuleMatches

            Erase a complete match.

            Instances For
              source
              def Aesop.ForwardRuleMatches.eraseMany (ms : Array ForwardRuleMatch) (ms' : ForwardRuleMatches) :
              ForwardRuleMatches

              Erase several complete matches.

              Instances For
                source
                def Aesop.ForwardRuleMatches.ofArray (ms : Array ForwardRuleMatch) :
                ForwardRuleMatches

                Build a ForwardRuleMatches structure containing the matches from ms.

                Instances For
                  source
                  def Aesop.ForwardRuleMatches.eraseHyps (hs : Std.HashSet Lean.FVarId) (ms : ForwardRuleMatches) :
                  ForwardRuleMatches

                  Erase matches containing any of the hypotheses hs from ms.

                  Instances For
                    source
                    def Aesop.ForwardRuleMatches.eraseHyp (h : Lean.FVarId) (ms : ForwardRuleMatches) :
                    ForwardRuleMatches

                    Erase matches containing the hypothesis h from ms.

                    Instances For
                      source
                      def Aesop.ForwardRuleMatches.update (newMatches : Array ForwardRuleMatch) (erasedHyps : Std.HashSet Lean.FVarId) (consumedForwardRuleMatches : Array ForwardRuleMatch) (forwardRuleMatches : ForwardRuleMatches) :
                      ForwardRuleMatches

                      Update the ForwardRuleMatches of a goal so that they are suitable for a child goal. newMatches are new forward rule matches obtained by updating the old goal's ForwardState with new hypotheses from the new goal. erasedHyps are the hypotheses from the old goal that no longer appear in the new goal. consumedForwardRuleMatches contains forward rule matches that were applied as rules to transform the old goal into the new goal.

                      Instances For
                        source
                        def Aesop.ForwardRuleMatches.normRules (ms : ForwardRuleMatches) :
                        Array NormRule

                        Get the norm rules corresponding to the norm rule matches.

                        Instances For
                          source
                          def Aesop.ForwardRuleMatches.safeRules (ms : ForwardRuleMatches) :
                          Array SafeRule

                          Get the safe rules corresponding to the safe rule matches.

                          Instances For
                            source
                            def Aesop.ForwardRuleMatches.unsafeRules (ms : ForwardRuleMatches) :
                            Array UnsafeRule

                            Get the unsafe rules corresponding to the unsafe rule matches.

                            Instances For
                              source
                              def Aesop.ForwardRuleMatches.size (ms : ForwardRuleMatches) :
                              Nat

                              O(n) Number of matches in ms.

                              Instances For