REPLICATE_CONV : conv
STRUCTURE
listLib
SYNOPSIS
Computes by inference the result of replicating an element a given number of times to form a list.
DESCRIPTION
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.
HOL  Trindemossen-1