EL_CONV : conv
STRUCTURE
listLib
SYNOPSIS
Computes by inference the result of indexing an element from a list.
DESCRIPTION
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
ELL_CONV
HOL
Kananaskis-10