		Search-engine friendly clone of the ACL2 documentation.

Integer-format

Integer-format->pair

Get the pair field from a integer-format.

Signature
(integer-format->pair x) → pair
Arguments: x — Guard (integer-formatp x).
Returns: pair — Type (uinteger+sinteger-formatp pair).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: integer-format->pair$inline

(defun integer-format->pair$inline (x)
 (declare (xargs :guard (integer-formatp x)))
 (declare (xargs :guard t))
 (let ((__function__ 'integer-format->pair))
  (declare (ignorable __function__))
  (mbe
   :logic
   (b*
    ((x (and t x))
     (pair (uinteger+sinteger-format-fix (cdr (std::da-nth 0 x)))))
    (if (uinteger-sinteger-bit-roles-wfp
             (uinteger-format->bits
                  (uinteger+sinteger-format->unsigned pair))
             (sinteger-format->bits
                  (uinteger+sinteger-format->signed pair)))
        pair
     (make-uinteger+sinteger-format
      :unsigned
      (make-uinteger-format :bits (list (uinteger-bit-role-value 0)
                                        (uinteger-bit-role-value 1))
                            :traps nil)
      :signed
      (make-sinteger-format :bits (list (sinteger-bit-role-value 0)
                                        (sinteger-bit-role-sign))
                            :signed (signed-format-twos-complement)
                            :traps nil))))
   :exec (cdr (std::da-nth 0 x)))))

Theorem: uinteger+sinteger-formatp-of-integer-format->pair

(defthm uinteger+sinteger-formatp-of-integer-format->pair
  (b* ((pair (integer-format->pair$inline x)))
    (uinteger+sinteger-formatp pair))
  :rule-classes :rewrite)

Theorem: integer-format->pair$inline-of-integer-format-fix-x

(defthm integer-format->pair$inline-of-integer-format-fix-x
  (equal (integer-format->pair$inline (integer-format-fix x))
         (integer-format->pair$inline x)))

Theorem: integer-format->pair$inline-integer-format-equiv-congruence-on-x

(defthm
   integer-format->pair$inline-integer-format-equiv-congruence-on-x
  (implies (integer-format-equiv x x-equiv)
           (equal (integer-format->pair$inline x)
                  (integer-format->pair$inline x-equiv)))
  :rule-classes :congruence)