		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Lognotu

Logical negation, unsigned version. (lognotu size i) is an unsigned logical not. It just truncates (lognot i) to size bits.

Signature
(lognotu size i) → nat
Arguments: size — Guard (and (integerp size) (<= 0 size)).; i — Guard (integerp i).
Returns: nat — Type (natp nat).

Definitions and Theorems

Function: lognotu$inline

(defun lognotu$inline (size i)
  (declare (xargs :guard (and (and (integerp size) (<= 0 size))
                              (integerp i))))
  (let ((__function__ 'lognotu))
    (declare (ignorable __function__))
    (loghead size (lognot i))))

Theorem: lognotu-type

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

Subtopics

Ihs/lognotu-lemmas: Lemmas about lognotu from the logops-lemmas book.
Lognotu-basics