----------------------------------------------------------------------
GENLIST_CONV                                                 (listLib)
----------------------------------------------------------------------
GENLIST_CONV : conv -> conv

SYNOPSIS
Computes by inference the result of generating a list from a function.

KEYWORDS
conversion, list.

DESCRIBE
For an arbitrary  function {f}, numeral constant {n} and conversion to evaluate {f} {conv}, the result of evaluating

   GENLIST_CONV conv “GENLIST f n”

is the theorem

   |- GENLIST f x = [x0;x1...xi...x(n-1)]

where each {xi} is the result of evaluating {conv “f i”}

EXAMPLE
Evaluating {GENLIST_CONV BETA_CONV “GENLIST (\n . n) 4”} will return
the following theorem:

   |- GENLIST (\n. n) 4 = [0; 1; 2; 3]




FAILURE
{GENLIST_CONV tm} fails if {tm} is not of the form described above, or if
any call {conv “f i”} fails.

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