### ACL2-COUNT

a commonly used measure for justifying recursion
Major Section: ACL2-BUILT-INS

`(Acl2-count x)`

returns a nonnegative integer that indicates the
``size'' of its argument `x`

.

All characters and symbols have `acl2-count 0`

. The `acl2-count`

of a
string is the number of characters in it, i.e., its length. The
`acl2-count`

of a `cons`

is one greater than the sum of the `acl2-count`

s
of the `car`

and `cdr`

. The `acl2-count`

of an integer is its absolute
value. The `acl2-count`

of a rational is the sum of the `acl2-count`

s
of the numerator and denominator. The `acl2-count`

of a complex
rational is one greater than the sum of the `acl2-count`

s of the real
and imaginary parts.