----------------------------------------------------------------------
LENGTH_CONV                                                  (listLib)
----------------------------------------------------------------------
LENGTH_CONV : conv

SYNOPSIS
Computes by inference the length of an object-language list.

KEYWORDS
conversion, list.

DESCRIBE
For any object language list of the form {“[x1;x2;...;xn]”}, where {x1},
{x2}, ..., {xn} are arbitrary terms of the same type, the result of evaluating

   LENGTH_CONV “LENGTH [x1;x2;...;xn]”

is the theorem

   |- LENGTH [x1;x2;...;xn] = n

where {n} is the numeral constant that denotes the length of the
list.

FAILURE
{LENGTH_CONV tm} fails if {tm} is not of the form {“LENGTH [x1;x2;...;xn]”}
or {“LENGTH []”}.

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