Syntax
where t is a switch;
The first form of the command is used to export names and expectations
so that they follow a label. Typically the label will be a string of
alphabetic characters preceded by the symbol `@' (this symbol is used as
the prefix recognised by [B/D] as implying that the remainder of a
string is a label name). The label is output as one line of text. The
second form of the command is identical to the first except that no
label is defined, and no label will be exported.
The list of element names and bases, N1, N2, ..., defines the
collection of elements to be exported. It is an error if the collection
so defined is empty. The elements in the collection are exported in the
order according to the ordering convention (so their ordering in the
EXPORT: command line is irrelevant). Each name is output on a
separate line, together with its expectation.
If no optional argument S
is given in the command, the expectations are taken from the default
expectation store. Otherwise, expectations are taken from expectation
store S.
are the names of elements or
bases; the optional argument S is an
expectation store number; and L is the name of a file label. Base notation (see
§6.2.4) can be used with the names.
