		Search-engine friendly clone of the ACL2 documentation.

Vl-initial

Make-vl-initial

Basic constructor macro for vl-initial structures.

Syntax

(make-vl-initial [:stmt <stmt>] 
                 [:atts <atts>] 
                 [:loc <loc>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-initial

(defmacro make-vl-initial (&rest args)
  (std::make-aggregate 'vl-initial
                       args '((:stmt) (:atts) (:loc))
                       'make-vl-initial
                       nil))

Function: vl-initial

(defun vl-initial (stmt atts loc)
 (declare (xargs :guard (and (vl-stmt-p stmt)
                             (vl-atts-p atts)
                             (vl-location-p loc))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-initial))
  (declare (ignorable __function__))
  (b* ((stmt (mbe :logic (vl-stmt-fix stmt)
                  :exec stmt))
       (atts (mbe :logic (vl-atts-fix atts)
                  :exec atts))
       (loc (mbe :logic (vl-location-fix loc)
                 :exec loc)))
   (cons
     :vl-initial (std::prod-cons stmt (std::prod-cons atts loc))))))