LENGTH_CONV
listLib.LENGTH_CONV : conv
Computes by inference the length of an object-language list.
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 []”.