REPLICATE_CONV

listLib.REPLICATE_CONV : conv

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

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.