		Search-engine friendly clone of the ACL2 documentation.

Representation-of-integers

Ushort-fix

Fixer for values of type unsigned short.

Signature
(ushort-fix x) → fixed-x
Arguments: x — Guard (ushortp x).
Returns: fixed-x — Type (ushortp fixed-x).

Definitions and Theorems

Function: ushort-fix

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

Theorem: ushortp-of-ushort-fix

(defthm ushortp-of-ushort-fix
  (b* ((fixed-x (ushort-fix x)))
    (ushortp fixed-x))
  :rule-classes :rewrite)

Theorem: ushort-fix-when-ushortp

(defthm ushort-fix-when-ushortp
  (implies (ushortp x)
           (equal (ushort-fix x) x)))