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.
Instances For
Equations
- Aesop.instInhabitedForwardRuleMatches = { default := { normMatches := default, safeMatches := default, unsafeMatches := default } }
Empty ForwardRuleMatches
.
Equations
- Aesop.ForwardRuleMatches.empty = { normMatches := ∅, safeMatches := ∅, unsafeMatches := ∅ }
Instances For
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.
Instances For
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
Instances For
Erase a complete match.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
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
Get the norm rules corresponding to the norm rule matches.
Equations
Instances For
Get the safe rules corresponding to the safe rule matches.
Equations
Instances For
Get the unsafe rules corresponding to the unsafe rule matches.
Equations
Instances For
O(n)
Number of matches in ms
.
Equations
- One or more equations did not get rendered due to their size.