GENLIST_CONV
listLib.GENLIST_CONV : conv -> conv
Computes by inference the result of generating a list from a function.
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.