Symbol mappings are used in translations, revealing reductions, fitting arguments, and views.
SYMB-MAP-ITEMS ::= symb-map-items SYMB-KIND SYMB-OR-MAP+ SYMB-OR-MAP ::= SYMB | SYMB-MAP SYMB-MAP ::= symb-map SYMB SYMB
A list of symbol maps SYMB-MAP-ITEMS with implicit kinds SYMB-KIND is written simply:
SY1 |-> SY'1, ..., SYn |-> SY'nThe sign displayed as a right arrow starting from a short vertical line in LaTeX is input as `|->'.
SYi |-> SY'i denotes the map that takes the symbol SYi to the symbol SY'i. The mapped symbols in the list must be distinct. Overloaded operation symbols and predicate symbols may be disambiguated by explicit qualification; when SYi is not qualified, the effect is that all operation or predicate symbols with the same name are mapped uniformly to SY'i.
Optionally, the list may be sectioned into sub-lists by inserting the keywords `sorts', `ops', `preds' (or their singular forms), which explicitly indicate that the subsequent symbols are of the corresponding kind:
sorts S1 |-> S'1, ..., ops O1 |-> O'1, ..., preds P1 |-> P'1, ...As with signature declarations in basic specifications, there is no restriction on the order of the various sections of the list.
An identity map `SYi |-> SYi' may be simply written `SYi'. Thus a symbol list may be regarded as a special case of a symbol mapping.
The list determines both the set of mapped symbols and the union of the listed symbol maps; the order in which symbol maps are listed is not significant (except regarding their position in relation to any specified kinds).