		Search-engine friendly clone of the ACL2 documentation.

Representation-of-integers

Sshort-fix

Fixer for values of type signed short.

Signature
(sshort-fix x) → fixed-x
Arguments: x — Guard (sshortp x).
Returns: fixed-x — Type (sshortp fixed-x).

Definitions and Theorems

Function: sshort-fix

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

Theorem: sshortp-of-sshort-fix

(defthm sshortp-of-sshort-fix
  (b* ((fixed-x (sshort-fix x)))
    (sshortp fixed-x))
  :rule-classes :rewrite)

Theorem: sshort-fix-when-sshortp

(defthm sshort-fix-when-sshortp
  (implies (sshortp x)
           (equal (sshort-fix x) x)))