Syntax
where e is a switch;
The first form of the command is used to export element expectations
(not preceded by the element names)
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 expectations for 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
expectation is output on a separate line.
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.
