Documentation

Aesop.Tree.Data.ForwardRuleMatches

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

Instances For
    Equations

    Empty ForwardRuleMatches.

    Equations
    Instances For

      Add a complete match.

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

        Erase a complete match.

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

          Erase matches containing any of the hypotheses hs from ms.

          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

              Erase matches containing the hypothesis h from ms.

              Equations
              Instances For
                def Aesop.ForwardRuleMatches.update (newMatches : Array ForwardRuleMatch) (erasedHyps : Std.HashSet Lean.FVarId) (consumedForwardRuleMatches : Array ForwardRuleMatch) (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.

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

                  O(n) Number of matches in ms.

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