		Search-engine friendly clone of the ACL2 documentation.

Bitops/extra-defs

Clearbit

Set X[n] := 0

Signature
(clearbit n x) → ans
Arguments: n — Bit position to clear to 0.
Guard (natp n).; x — Starting value.
Guard (integerp x).
Returns: ans — Type (integerp ans).

Definitions and Theorems

Function: clearbit

(defun clearbit (n x)
  (declare (xargs :guard (and (natp n) (integerp x))))
  (let ((__function__ 'clearbit))
    (declare (ignorable __function__))
    (let ((n (lnfix n)) (x (lifix x)))
      (logand (lognot (ash 1 n)) x))))

Theorem: integerp-of-clearbit

(defthm acl2::integerp-of-clearbit
  (b* ((ans (clearbit n x)))
    (integerp ans))
  :rule-classes :type-prescription)

Theorem: nat-equiv-implies-equal-clearbit-1

(defthm nat-equiv-implies-equal-clearbit-1
  (implies (nat-equiv n n-equiv)
           (equal (clearbit n x)
                  (clearbit n-equiv x)))
  :rule-classes (:congruence))

Theorem: int-equiv-implies-equal-clearbit-2

(defthm int-equiv-implies-equal-clearbit-2
  (implies (int-equiv x x-equiv)
           (equal (clearbit n x)
                  (clearbit n x-equiv)))
  :rule-classes (:congruence))