File: itlist2.doc

package info (click to toggle)
hol88 2.02.19940316dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 65,816 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (29 lines) | stat: -rw-r--r-- 553 bytes parent folder | download | duplicates (11) 
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
 
\DOC itlist2

\TYPE {itlist2 : (((* # **) -> *** -> ***) -> (* list # ** list) -> *** -> ***)}

\SYNOPSIS
Applies a paired function between adjacent elements of 2 lists.

\KEYWORDS
list.

\DESCRIBE
{itlist2 f ([x1;...;xn],[y1;...;yn]) z} returns
{
   f (x1,y1) (f (x2,y2) ... (f (xn,yn) z)...)
}
\noindent It returns {z} if both lists are empty.

\FAILURE
Fails with {itlist2} if the two lists are of different lengths.

\EXAMPLE
{
#itlist2 (\(x,y) z. (x * y) + z) ([1;2],[3;4]) 0;;
11 : int
}
\SEEALSO
itlist, rev_itlist, end_itlist, uncurry.

\ENDDOC