ELL_CONV : conv

- 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 evaluatingis the theorem
ELL_CONV “ELL k [xn-1;...;xk;...;x0]”

where k must not be greater then the length of the list. Note that ELL indexes the list elements from the tail end.|- ELL k [xn-1;...;xk;...;x0] = xk

- 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

HOL Kananaskis-14