		Search-engine friendly clone of the ACL2 documentation.

Vl-final

Make-vl-final

Basic constructor macro for vl-final structures.

Syntax

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

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-final

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

Function: vl-final

(defun vl-final (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-final))
  (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-final (std::prod-cons stmt (std::prod-cons atts loc))))))