Sets of complete matches for norm/safe/unsafe rules.
- normMatches : Lean.PHashSet ForwardRuleMatch
Complete matches of norm rules.
- safeMatches : Lean.PHashSet ForwardRuleMatch
Complete matches of safe rules.
- unsafeMatches : Lean.PHashSet ForwardRuleMatch
Complete matches of unsafe rules.
Empty ForwardRuleMatches
.
Equations
- Aesop.ForwardRuleMatches.instEmptyCollection = { emptyCollection := Aesop.ForwardRuleMatches.empty }
Add a complete match.
Equations
- One or more equations did not get rendered due to their size.
Add several complete matches.
Equations
- Aesop.ForwardRuleMatches.insertMany ms ms' = Array.foldl (fun (ms' : Aesop.ForwardRuleMatches) (m : Aesop.ForwardRuleMatch) => Aesop.ForwardRuleMatches.insert m ms') ms' ms
Erase a complete match.
Equations
- One or more equations did not get rendered due to their size.
Erase several complete matches.
Equations
- Aesop.ForwardRuleMatches.eraseMany ms ms' = Array.foldl (fun (ms' : Aesop.ForwardRuleMatches) (m : Aesop.ForwardRuleMatch) => Aesop.ForwardRuleMatches.erase m ms') ms' ms
Build a ForwardRuleMatches
structure containing the matches from ms
.
Equations
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.
Erase matches containing the hypothesis h
from ms
.
Equations
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.
Get the norm rules corresponding to the norm rule matches.
Get the safe rules corresponding to the safe rule matches.
Get the unsafe rules corresponding to the unsafe rule matches.
O(n)
Number of matches in ms
.
Equations
- One or more equations did not get rendered due to their size.