Major Section: ACL2-BUILT-INS
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.)
To see the ACL2 definition of this function, see pf.