/usr/share/hol88-2.02.19940316/help/ENTRIES/funpow.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 33 34 35 36 37 38 39 40 41 42 43 44 | \DOC funpow
\TYPE {funpow : (int -> (* -> *) -> * -> *)}
\SYNOPSIS
Iterates a function a fixed number of times.
\DESCRIBE
{funpow n f x} applies {f} to {x}, {n} times, giving the result {f (f ... (f
x)...)} where the number of {f}'s is {n}. {funpow 0 f x} returns {x}. If {n} is
negative, {funpow n f x} will either fail or loop indefinitely, depending on
the values of {f} and {x}.
\FAILURE
{funpow n f x} fails if any of the {n} applications of f fail.
\EXAMPLE
Apply {tl} three times to a list:
{
#funpow 3 tl [1;2;3;4;5];;
[4; 5] : int list
}
\noindent Apply {tl} zero times:
{
#funpow 0 tl [1;2;3;4;5];;
[1; 2; 3; 4; 5] : int list
}
\noindent Apply {tl} six times to a list of only five elements:
{
#funpow 6 tl [1;2;3;4;5];;
evaluation failed tl
}
\noindent Next, an application of {funpow} in which the integer argument is
negative. Since the function cannot be applied to the argument an arbitrary
number of times, the application of {funpow} fails.
{
#funpow (-1) tl [1;2;3;4;5];;
evaluation failed tl
}
\noindent An example that causes indefinite looping:
{
#funpow (-1) I [1;2;3;4;5];;
}
\ENDDOC
|