/usr/share/hol88-2.02.19940316/help/ENTRIES/<<.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 | \DOC <<
\TYPE {$<< : ((* # **) -> bool)}
\SYNOPSIS
Performs a lexical comparison of values.
\KEYWORDS
address, order.
\DESCRIBE
{$<<} performs a fast ordering on values. It is substitutive with
respect to equality in ML (i.e. if {x << y} and {x = x'} and {y = y'}
then {x' << y'}).
\FAILURE
Never fails.
\USES
It is often useful, for example in normalizing terms in some way, to be able to
impose some arbitrary (but definite) ordering on ML values.
\SEEALSO
=.
\ENDDOC
|