/usr/share/hol88-2.02.19940316/help/ENTRIES/maptok.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 27 28 29 30 31 32 | \DOC maptok
\TYPE {maptok : ((string -> *) -> string -> * list)}
\SYNOPSIS
Maps a function over the constituent words of a string.
\DESCRIBE
{maptok f s} first splits the string {s} into a list of substrings, and then
maps the function {f} over that list. Splitting of the string occurs at each
sequence of blanks and carriage returns (white space). This white space does
not appear in the list of substrings. Leading and trailing white space in the
input string is also thrown away.
\FAILURE
Fails if one of the applications of {f} to a substring fails.
\EXAMPLE
{
#maptok explode ` the cat sat `;;
[[`t`; `h`; `e`]; [`c`; `a`; `t`]; [`s`; `a`; `t`]] : string list list
}
\USES
Useful when wanting to map a function over a list of constant strings.
Instead of using {map f [`string1`;...;`stringn`]} one can use:
{
(maptok f `string1 ... stringn`)
}
\SEEALSO
words, word_separators, words2, map.
\ENDDOC
|