LASTN_CONV : conv

- STRUCTURE
- SYNOPSIS
- Computes by inference the result of taking the last n elements of a list.
- DESCRIPTION
- For any object language list of the form “[x0;...x(n-k);...;x(n-1)]” , the result of evaluatingis the theorem
LASTN_CONV “LASTN k [x0;...x(n-k);...;x(n-1)]”

|- LASTN k [x0;...;x(n-k);...;x(n-1)] = [x(n-k);...;x(n-1)]

- FAILURE
- LASTN_CONV tm fails if tm is not of the form described above, or k is greater than the length of the list.

HOL Kananaskis-14