----------------------------------------------------------------------
BUTLAST_CONV                                                 (listLib)
----------------------------------------------------------------------
BUTLAST_CONV : conv

SYNOPSIS
Computes by inference the result of stripping the last element of a list.

KEYWORDS
conversion, list.

DESCRIBE
For any object language list of the form {“[x0;...x(n-1)]”} ,
the result of evaluating

   BUTLAST_CONV “BUTLAST [x0;...;x(n-1)]”

is the theorem

   |- BUTLAST [x0;...;x(n-1)] = [x0;...; x(n-2)]




FAILURE
{BUTLAST_CONV tm} fails if {tm} is an empty list.

----------------------------------------------------------------------