		Search-engine friendly clone of the ACL2 documentation.

Len

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

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

Function: len

(defun len (x)
  (declare (xargs :guard t))
  (if (consp x) (+ 1 (len (cdr x))) 0))

Subtopics

Std/lists/len: Lemmas about len available in the std/lists library.