LAST_CONV : conv
STRUCTURE
SYNOPSIS
Computes by inference the result of taking the last element of a list.
DESCRIPTION
For any object language list of the form “[x0;...x(n-1)]” , the result of evaluating
   LAST_CONV “LAST [x0;...;x(n-1)]”
is the theorem
   |- LAST [x0;...;x(n-1)] = x(n-1)

FAILURE
LAST_CONV tm fails if tm is an empty list.
HOL  Kananaskis-11