		Search-engine friendly clone of the ACL2 documentation.

A4vec

Make-a4vec

Basic constructor macro for a4vec structures.

Syntax

(make-a4vec [:upper <upper>] 
            [:lower <lower>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-a4vec

(defmacro make-a4vec (&rest args)
  (std::make-aggregate 'a4vec
                       args '((:upper) (:lower))
                       'make-a4vec
                       nil))

Function: a4vec

(defun a4vec (upper lower)
  (declare (xargs :guard (and (true-listp upper)
                              (true-listp lower))))
  (declare (xargs :guard t))
  (let ((__function__ 'a4vec))
    (declare (ignorable __function__))
    (b* ((upper (mbe :logic (list-fix upper)
                     :exec upper))
         (lower (mbe :logic (list-fix lower)
                     :exec lower)))
      (cons upper lower))))