ACL2-COUNT
a commonly used measure for justifying recursion
Major Section: MISCELLANEOUS
(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-counts
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-counts
of the numerator and denominator. The acl2-count of a complex
rational is one greater than the sum of the acl2-counts of the real
and imaginary parts.
