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 [CHANGED:] as if all (sort, operation, or predicate) symbols declared with the same name in the current environment [] 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 f1 |-> f'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 [CHANGED:] a set of qualified symbols, obtained from the first components of the listed symbol maps with reference to a given signature, together with a mapping of these symbols to qualified symbols obtained from the second components 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).