		Search-engine friendly clone of the ACL2 documentation.

Make-int

Basic constructor macro for int structures.

Syntax

(make-int [:size <size>] 
          [:value <value>])

This is the usual way to construct int structures. It simply conses together a structure with the specified fields.

This macro generates a new int structure from scratch. See also change-int, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-int

(defmacro make-int (&rest args)
  (std::make-aggregate 'int
                       args '((:size) (:value))
                       'make-int
                       nil))

Function: int

(defun int (size value)
  (declare (xargs :guard (and (bit-size-p size)
                              (integerp value))))
  (declare (xargs :guard (signed-byte-p size value)))
  (let ((__function__ 'int))
    (declare (ignorable __function__))
    (b* ((size (mbe :logic (bit-size-fix size)
                    :exec size))
         (value (mbe :logic (ifix value) :exec value)))
      (let ((value (mbe :logic (signed-byte-fix size value)
                        :exec value)))
        (cons :int (list size value))))))