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.
(defun length (x)
(declare (xargs :guard (if (true-listp x) t (stringp x))))
(if (stringp x)
(len (coerce x 'list))