		Search-engine friendly clone of the ACL2 documentation.

Values

Make-int-value

Makes an integer value or an error.

Signature
(make-int-value int-value-kind int-vv) → result
Arguments: int-value-kind — Guard (symbolp int-value-kind).; int-vv — Guard (integerp int-vv).
Returns: result — Type (value-resultp result).

Definitions and Theorems

Function: make-int-value

(defun make-int-value (int-value-kind int-vv)
  (declare (xargs :guard (and (symbolp int-value-kind)
                              (integerp int-vv))))
  (let ((__function__ 'make-int-value))
    (declare (ignorable __function__))
    (let ((err (reserrf (list :make-int-value
                              int-value-kind int-vv))))
      (case int-value-kind
        (:u8 (if (and (<= 0 int-vv)
                      (<= int-vv *greatest-u8*))
                 (value-u8 int-vv)
               err))
        (:u16 (if (and (<= 0 int-vv)
                       (<= int-vv *greatest-u16*))
                  (value-u16 int-vv)
                err))
        (:u32 (if (and (<= 0 int-vv)
                       (<= int-vv *greatest-u32*))
                  (value-u32 int-vv)
                err))
        (:u64 (if (and (<= 0 int-vv)
                       (<= int-vv *greatest-u64*))
                  (value-u64 int-vv)
                err))
        (:u128 (if (and (<= 0 int-vv)
                        (<= int-vv *greatest-u128*))
                   (value-u128 int-vv)
                 err))
        (:i8 (if (and (<= *most-negative-i8* int-vv)
                      (<= int-vv *most-positive-i8*))
                 (value-i8 int-vv)
               err))
        (:i16 (if (and (<= *most-negative-i16* int-vv)
                       (<= int-vv *most-positive-i16*))
                  (value-i16 int-vv)
                err))
        (:i32 (if (and (<= *most-negative-i32* int-vv)
                       (<= int-vv *most-positive-i32*))
                  (value-i32 int-vv)
                err))
        (:i64 (if (and (<= *most-negative-i64* int-vv)
                       (<= int-vv *most-positive-i64*))
                  (value-i64 int-vv)
                err))
        (:i128 (if (and (<= *most-negative-i128* int-vv)
                        (<= int-vv *most-positive-i128*))
                   (value-i128 int-vv)
                 err))
        (t err)))))

Theorem: value-resultp-of-make-int-value

(defthm value-resultp-of-make-int-value
  (b* ((result (make-int-value int-value-kind int-vv)))
    (value-resultp result))
  :rule-classes :rewrite)