Major Section: ACL2-BUILT-INS
For non-negative integers, (integer-length i) is the minimum number
of bits needed to represent the integer. Any integer can be
represented as a signed two's complement field with a minimum of
(+ (integer-length i) 1) bits.
The guard for integer-length requires its argument to be an
integer. Integer-length is defined in Common Lisp. See any
Common Lisp documentation for more information.
To see the ACL2 definition of this function, see pf.
