		Search-engine friendly clone of the ACL2 documentation.

Vl-iskipinfo

Make-vl-iskipinfo

Basic constructor macro for vl-iskipinfo structures.

Syntax

(make-vl-iskipinfo [:controller <controller>] 
                   [:misses <misses>] 
                   [:hits <hits>] 
                   [:len <len>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-iskipinfo

(defmacro make-vl-iskipinfo (&rest args)
  (std::make-aggregate 'vl-iskipinfo
                       args
                       '((:controller) (:misses) (:hits) (:len))
                       'make-vl-iskipinfo
                       nil))

Function: vl-iskipinfo

(defun vl-iskipinfo (controller misses hits len)
 (declare (xargs :guard (and (maybe-stringp controller)
                             (vl-locationlist-p misses)
                             (vl-locationlist-p hits)
                             (natp len))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-iskipinfo))
  (declare (ignorable __function__))
  (b* ((controller (mbe :logic (maybe-string-fix controller)
                        :exec controller))
       (misses (mbe :logic (vl-locationlist-fix misses)
                    :exec misses))
       (hits (mbe :logic (vl-locationlist-fix hits)
                  :exec hits))
       (len (mbe :logic (nfix len) :exec len)))
   (cons
    :vl-iskipinfo (std::prod-cons (std::prod-cons controller misses)
                                  (std::prod-cons hits len))))))