Documentation

Aesop.Index.RulePattern

@[reducible, inline]

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.

                    Instances For

                      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

                                      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.

                                                  Equations
                                                    Instances For