----------------------------------------------------------------------
MAP2_CONV                                                    (listLib)
----------------------------------------------------------------------
MAP2_CONV : conv -> conv

SYNOPSIS
Compute the result of mapping a binary function down two lists.

KEYWORDS
conversion, list.

DESCRIBE
The function {MAP2_CONV} is a conversion for computing the result
of mapping a binary function {f:ty1->ty2->ty3} down two lists
{“[l11;...;l1n]”} whose elements are of type {ty1} and
{“[l21;...;l2n]”} whose elements are of type {ty2}.  The lengths of
the two lists must be identical. The first
argument to {MAP2_CONV} is expected to be a conversion
that computes the result of applying the function {f} to a pair of
corresponding elements of these lists. When applied to a term
{“f l1i l2i”}, this conversion should return a theorem of the form
{|- (f l1i l2i) = ri}, where {ri} is the result of applying the function
{f} to the elements {l1i} and {l2i}.

Given an appropriate {conv}, the conversion {MAP2_CONV conv} takes a
term of the form {“MAP2 f [l11;...;dl2tn] [l21;...;l2n]”} and returns
the theorem

   |- MAP2 f [l11;...;l1n] [l21;...;l2n] = [r1;...;rn]

where {conv “f l1i l2i”} returns {|- (f l1i l2i) = ri} for
{i} from {1} to {n}.

EXAMPLE
The following is a very simple example in which the corresponding
elements from the two lists are summed to form the resulting list:

   - load_library_in_place num_lib;
   - MAP2_CONV Num_lib.ADD_CONV “MAP2 $+ [1;2;3] [1;2;3]”;
   |- MAP2 $+ [1;2;3] [1;2;3] = [2;4;6]


FAILURE
{MAP2_CONV conv} fails if applied to a term not of the form
described above.  An application of {MAP2_CONV conv} to a term
{“MAP2 f [l11;...;l1n] [l21;...;l2n]”} fails unless for all {i} where {1<=i<=n}
evaluating {conv “f l1i l2i”} returns {|- (f l1i l2i) = ri} for some {ri}.

SEEALSO
listLib.MAP_CONV.

----------------------------------------------------------------------