		Search-engine friendly clone of the ACL2 documentation.

Vl-immdeps

Make-vl-immdeps

Basic constructor macro for vl-immdeps structures.

Syntax

(make-vl-immdeps [:all-okp <all-okp>] 
                 [:deps <deps>] 
                 [:warnings <warnings>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-immdeps

(defmacro make-vl-immdeps (&rest args)
  (std::make-aggregate 'vl-immdeps
                       args
                       '((:all-okp . t) (:deps) (:warnings))
                       'make-vl-immdeps
                       nil))

Function: vl-immdeps

(defun vl-immdeps (all-okp deps warnings)
 (declare (xargs :guard (and (booleanp all-okp)
                             (string-listp deps)
                             (vl-warninglist-p warnings))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-immdeps))
  (declare (ignorable __function__))
  (b* ((all-okp (mbe :logic (acl2::bool-fix all-okp)
                     :exec all-okp))
       (deps (mbe :logic (string-list-fix deps)
                  :exec deps))
       (warnings (mbe :logic (vl-warninglist-fix warnings)
                      :exec warnings)))
   (cons
     :vl-immdeps (std::prod-cons all-okp
                                 (std::prod-cons deps warnings))))))