Documentation

Aesop.Tree.Data.ForwardRuleMatches

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

Instances For
Equations

Empty ForwardRuleMatches.

Equations

Add a complete match.

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

Erase a complete match.

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

Erase matches containing any of the hypotheses hs from ms.

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
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.

O(n) Number of matches in ms.

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