Length of a list
Len returns the length of a list.
A Common Lisp function that is appropriate for both strings and proper
lists is length; see length. The guard for len is
(Low-level implementation note. ACL2 provides a highly-optimized
implementation of len, which is tail-recursive and fixnum-aware, that
differs from its simple ACL2 definition.)
(defun len (x)
(declare (xargs :guard t))
(if (consp x) (+ 1 (len (cdr x))) 0))
- Lemmas about len available in the std/lists library.