Index for forward rules.
- tree : Lean.Meta.DiscrTree (ForwardRule × PremiseIndex)
Maps expressions
T
to all tuples(r, i)
wherer : ForwardRule
,i : PremiseIndex
and thei
-th argument of the type ofr.expr
(counting from zero) likely unifies withT
. - nameToRule : Lean.PHashMap RuleName ForwardRule
Indexes the forward rules contained in
tree
by name. - constRules : Lean.PHashSet ForwardRule
Constant forward rules, i.e. forward rules that have no premises and no rule pattern.
Instances For
Equations
Equations
Instances For
Trace the rules contained in idx
if traceOpt
is enabled.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Merge two indices.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Insert a forward rule into the ForwardIndex
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Get the forward rules whose maximal premises likely unify with e
.
Each returned pair (r, i)
contains a rule r
and the index i
of the premise
of r
that likely unifies with e
.
Equations
- idx.get e = Aesop.getUnify idx.tree e
Instances For
Get the forward rule with the given rule name.
Equations
- Aesop.ForwardIndex.getRuleWithName? n idx = idx.nameToRule[n]
Instances For
Get forward rule matches for the constant forward rules (i.e., those with no premises and no rule pattern). Accordingly, the returned matches contain no hypotheses.
Equations
- idx.getConstRuleMatches = Lean.PersistentHashSet.fold (fun (ms : Array Aesop.ForwardRuleMatch) (r : Aesop.ForwardRule) => ms.push { rule := r, «match» := ∅ }) #[] idx.constRules