		Search-engine friendly clone of the ACL2 documentation.

Length

Length of a string or proper list

Length is the function for determining the length of a sequence. In ACL2, the argument is required to be either a true-listp or a string.

For a similar function that is logically defined to be equal to zero on any atom, including any string, see len.

Length is a Common Lisp function. See any Common Lisp documentation for more information.

Function: length

(defun length (x)
  (declare (xargs :guard (if (true-listp x) t (stringp x))))
  (if (stringp x)
      (len (coerce x 'list))
    (len x)))