/usr/share/hol88-2.02.19940316/help/ENTRIES/remove.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 | \DOC remove
\TYPE {remove : ((* -> bool) -> * list -> (* # * list))}
\SYNOPSIS
Separates the first element of a list to satisfy a predicate from the rest of
the list.
\FAILURE
Fails with {hd} if no element satisfes the predicate. This will always be the
case for an empty list.
\EXAMPLE
{
#remove (\x. x = 3) [1;2;3;4;5;6];;
(3, [1; 2; 4; 5; 6]) : (int # int list)
}
\SEEALSO
partition, filter.
\ENDDOC
|