----------------------------------------------------------------------
ELL_CONV                                                     (listLib)
----------------------------------------------------------------------
ELL_CONV : conv

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

KEYWORDS
conversion, list.

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

   ELL_CONV “ELL k [xn-1;...;xk;...;x0]”

is the theorem

   |- ELL k [xn-1;...;xk;...;x0] = xk

where {k} must not be greater then the length of the list.
Note that {ELL} indexes the list elements from the tail end.

FAILURE
{ELL_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.EL_CONV.

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