----------------------------------------------------------------------
EL_CONV                                                      (listLib)
----------------------------------------------------------------------
EL_CONV : conv

SYNOPSIS
Computes by inference the result of indexing an element from a list.

KEYWORDS
conversion, list.

DESCRIBE
For any object language list of the form {“[x0;...xk;...;xn]”} ,
the result of evaluating

   EL_CONV “EL k [x0;...xk;...;xn]”

is the theorem

   |- EL k [x0;...;xk;...;xn] = xk




FAILURE
{EL_CONV tm} fails if {tm} is not of the form described above,
or {k} is not less than the length of the list.

SEEALSO
listLib.ELL_CONV.

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