INTEGER-LENGTH

number of bits in two's complement integer representation
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.