		Search-engine friendly clone of the ACL2 documentation.

Representation-of-integers

Ullong-fix

Fixer for values of type unsigned long long.

Signature
(ullong-fix x) → fixed-x
Arguments: x — Guard (ullongp x).
Returns: fixed-x — Type (ullongp fixed-x).

Definitions and Theorems

Function: ullong-fix

(defun ullong-fix (x)
  (declare (xargs :guard (ullongp x)))
  (let ((__function__ 'ullong-fix))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((get (ullong-integer-fix (std::da-nth 0 (cdr x)))))
           (cons :ullong (list get)))
         :exec x)))

Theorem: ullongp-of-ullong-fix

(defthm ullongp-of-ullong-fix
  (b* ((fixed-x (ullong-fix x)))
    (ullongp fixed-x))
  :rule-classes :rewrite)

Theorem: ullong-fix-when-ullongp

(defthm ullong-fix-when-ullongp
  (implies (ullongp x)
           (equal (ullong-fix x) x)))