		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Logmask

(logmask size) creates a low-order, size-bit mask.

Signature
(logmask size) → nat
Arguments: size — Guard (natp size).
Returns: nat — Type (natp nat).

In languages like C, this might be written as (1 << size) - 1.

Definitions and Theorems

Function: logmask$inline

(defun logmask$inline (size)
  (declare (xargs :guard (natp size)))
  (let ((__function__ 'logmask))
    (declare (ignorable __function__))
    (mbe :logic (- (expt2 size) 1)
         :exec (the unsigned-byte
                    (1- (the unsigned-byte (ash 1 size)))))))

Theorem: logmask-type

(defthm logmask-type
  (b* ((nat (logmask$inline size)))
    (natp nat))
  :rule-classes :type-prescription)