listLib.ELL

STRUCTURE

SYNOPSIS

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

DESCRIPTION

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