----------------------------------------------------------------------
REPLICATE_CONV                                               (listLib)
----------------------------------------------------------------------
REPLICATE_CONV : conv

SYNOPSIS
Computes by inference the result of replicating an element a given number of
times to form a list.

KEYWORDS
conversion, list.

DESCRIBE
For an arbitrary expression {x} and numeral constant {n}, the result of
evaluating

   REPLICATE_CONV “REPLICATE n x”

is the theorem

   |- REPLICATE n x = [x;x;...;x]

where the list{[x;x;...;x]} is of length {n}.

EXAMPLE
Evaluating {REPLICATE_CONV “REPLICATE 3 [0;1;2;3]”} will return
the following theorem:

   |- REPLICATE 3 [0;1;2;3] = [[0;1;2;3]; [0;1;2;3]; [0;1;2;3]]




FAILURE
{REPLICATE_CONV tm} fails if {tm} is not of the form described above.

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