EL_CONV : conv

- STRUCTURE
- 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 evaluatingis the theorem
EL_CONV “EL k [x0;...xk;...;xn]”

|- 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

HOL Kananaskis-14