A map from rule names to rule pattern substitutions. When run on a goal, the rule pattern index returns such a map.
Equations
Instances For
Insert an array of rule pattern substitutions into a rule pattern substitution map.
Equations
Instances For
Build a rule pattern substitution map from an array of substitutions.
Equations
Instances For
Convert a rule pattern substitution map to a flat array of substitutions.
Equations
Instances For
An entry of the rule pattern index.
- name : RuleName
The name of the rule to which the pattern belongs.
- pattern : RulePattern
The rule's pattern. We assume that there is at most one pattern per rule.
Instances For
A rule pattern index. Maps expressions e
to rule patterns that likely
unify with e
.
- tree : Lean.Meta.DiscrTree Entry
The index.
- isEmpty : Bool
true
iff the index contains no patterns.
Instances For
Equations
Add a rule pattern to the index.
Equations
Instances For
Merge two rule pattern indices. Patterns that appear in both indices appear twice in the result.
Equations
Instances For
Get rule pattern substitutions for the patterns that match e
.
Equations
Instances For
Get all substitutions of the rule patterns that match a subexpression of
e
. Subexpressions containing bound variables are not considered. The returned
array may contain duplicates.
Equations
Instances For
Equations
Instances For
Get all substitutions of the rule patterns that match a subexpression of
e
. Subexpressions containing bound variables are not considered. The returned
array may contain duplicates.
Equations
Instances For
Get all substitutions of the rule patterns that match a subexpression of the given local declaration. Subexpressions containing bound variables are not considered.
Equations
Instances For
Get all substitutions of the rule patterns that match a subexpression of the given local declaration. Subexpressions containing bound variables are not considered.
Equations
Instances For
Get all substitutions of the rule patterns that match a subexpression of a hypothesis or the target. Subexpressions containing bound variables are not considered.