		Search-engine friendly clone of the ACL2 documentation.

Vl-lucidstate

Make-vl-lucidstate

Basic constructor macro for vl-lucidstate structures.

Syntax

(make-vl-lucidstate [:db <db>] 
                    [:paramsp <paramsp>] 
                    [:generatesp <generatesp>] 
                    [:warnings <warnings>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-lucidstate

(defmacro make-vl-lucidstate (&rest args)
  (std::make-aggregate 'vl-lucidstate
                       args
                       '((:db)
                         (:paramsp)
                         (:generatesp)
                         (:warnings))
                       'make-vl-lucidstate
                       nil))

Function: vl-lucidstate

(defun vl-lucidstate (db paramsp generatesp warnings)
  (declare (xargs :guard (and (vl-luciddb-p db)
                              (booleanp paramsp)
                              (booleanp generatesp)
                              (vl-warninglist-p warnings))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-lucidstate))
    (declare (ignorable __function__))
    (b* ((db (mbe :logic (vl-luciddb-fix db)
                  :exec db))
         (paramsp (mbe :logic (acl2::bool-fix paramsp)
                       :exec paramsp))
         (generatesp (mbe :logic (acl2::bool-fix generatesp)
                          :exec generatesp))
         (warnings (mbe :logic (vl-warninglist-fix warnings)
                        :exec warnings)))
      (std::prod-cons (std::prod-cons db paramsp)
                      (std::prod-cons generatesp warnings)))))