----------------------------------------------------------------------
APPEND_CONV                                                  (listLib)
----------------------------------------------------------------------
APPEND_CONV : conv

SYNOPSIS
Computes by inference the result of appending two object-language lists.

KEYWORDS
conversion, list.

DESCRIBE
For any pair of object language lists of the form {“[x1;...;xn]”} and
{“[y1;...;ym]”}, the result of evaluating

   APPEND_CONV “APPEND [x1;...;xn] [y1;...;ym]”

is the theorem

   |- APPEND [x1;...;xn] [y1;...;ym] = [x1;...;xn;y1;...;ym]

The length of either list (or both) may be 0.

FAILURE
{APPEND_CONV tm} fails if {tm} is not of the form {“APPEND l1 l2”}, where
{l1} and {l2} are (possibly empty) object-language lists of the forms
{“[x1;...;xn]”} and {“[y1;...;ym]”}.

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