From release 2.3.0 onward, it is possible to specify secondary indices within a rewriting system. This makes it possible to invoke other rewriting systems within the execution of another, while retaining the state caching optimizations throughout.
There are two forms of secondary index: internal index and external index. Internal indices are stored directly within a rewrite term and require the user to pre-allocate space for each term. In contrast, external indices are stored in a separate data structure such as a hash table.
The syntax of secondary index declarations is as follows:
Index_Decl ::= index: Index_Spec, ΕΊ , Index_Spec ; Index_Spec ::= Type_Exp = none Disable indexing | Type_Exp = Id Internal index | Type_Exp = extern Id External index