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.