		Search-engine friendly clone of the ACL2 documentation.

ACL2-count

A commonly used measure for justifying recursion

(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.

Function: acl2-count

(defun acl2-count (x)
  (declare (xargs :guard t))
  (if (consp x)
      (+ 1 (acl2-count (car x))
         (acl2-count (cdr x)))
    (if (rationalp x)
        (if (integerp x)
            (integer-abs x)
          (+ (integer-abs (numerator x))
             (denominator x)))
      (if (complex/complex-rationalp x)
          (+ 1 (acl2-count (realpart x))
             (acl2-count (imagpart x)))
        (if (stringp x) (length x) 0)))))

Subtopics

Two-nats-measure: An ordinal measure for admitting functions: lexicographic ordering of two natural numbers.
Nat-list-measure: An ordinal measure for admitting functions: lexicographic ordering of a list of natural numbers.