----------------------------------------------------------------------
SEG_CONV                                                     (listLib)
----------------------------------------------------------------------
SEG_CONV : conv

SYNOPSIS
Computes by inference the result of taking a segment of a list.

KEYWORDS
conversion, list.

DESCRIBE
For any object language list of the form {“[x0;...x(n-1)]”} ,
the result of evaluating

   SEG_CONV “SEG m k [x0;...;x(n-1)]”

is the theorem

   |- SEG m k [x0;...;x(n-1)] = [xk;...;x(m+k-1)]




FAILURE
{SEG_CONV tm} fails if {tm} is not in the form described above or the
indexes {m} and {k} are not in the correct range, i.e., {m + k <= n}.

EXAMPLE
Evaluating the expression

   SEG_CONV “SEG 2 3[0;1;2;3;4;5]”;

returns the following theorem

   |- SEG 2 3[0;1;2;3;4;5] = [3;4]


SEEALSO
listLib.FIRSTN_CONV, listLib.LASTN_CONV, listLib.BUTFIRSTN_CONV,
listLib.BUTLASTN_CONV, listLib.LAST_CONV, listLib.BUTLAST_CONV.

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