LENGTH_CONV : conv

- STRUCTURE
- SYNOPSIS
- Computes by inference the length of an object-language list.
- DESCRIPTION
- 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 evaluatingis the theorem
LENGTH_CONV “LENGTH [x1;x2;...;xn]”

where n is the numeral constant that denotes the length of the list.|- LENGTH [x1;x2;...;xn] = n

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

HOL Kananaskis-14