		Search-engine friendly clone of the ACL2 documentation.

Vl-explicitvalueparam

Make-vl-explicitvalueparam

Basic constructor macro for vl-explicitvalueparam structures.

Syntax

(make-vl-explicitvalueparam [:type <type>] 
                            [:default <default>] 
                            [:final-value <final-value>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-explicitvalueparam

(defmacro make-vl-explicitvalueparam (&rest args)
  (std::make-aggregate 'vl-explicitvalueparam
                       args
                       '((:type) (:default) (:final-value))
                       'make-vl-explicitvalueparam
                       nil))

Function: vl-explicitvalueparam

(defun vl-explicitvalueparam (type default final-value)
 (declare (xargs :guard (and (vl-datatype-p type)
                             (vl-maybe-expr-p default)
                             (sv::maybe-4vec-p final-value))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-explicitvalueparam))
   (declare (ignorable __function__))
   (b* ((type (mbe :logic (vl-datatype-fix type)
                   :exec type))
        (default (mbe :logic (vl-maybe-expr-fix default)
                      :exec default))
        (final-value (mbe :logic (sv::maybe-4vec-fix final-value)
                          :exec final-value)))
     (cons :vl-explicitvalueparam
           (std::prod-cons type
                           (std::prod-cons default final-value))))))