		Search-engine friendly clone of the ACL2 documentation.

Vl-scopeexpr-colon

Make-vl-scopeexpr-colon

Basic constructor macro for vl-scopeexpr-colon structures.

Syntax

(make-vl-scopeexpr-colon [:first <first>] 
                         [:paramargs <paramargs>] 
                         [:rest <rest>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-scopeexpr-colon

(defmacro make-vl-scopeexpr-colon (&rest args)
  (std::make-aggregate 'vl-scopeexpr-colon
                       args '((:first) (:paramargs) (:rest))
                       'make-vl-scopeexpr-colon
                       nil))

Function: vl-scopeexpr-colon

(defun vl-scopeexpr-colon (first paramargs rest)
  (declare (xargs :guard (and (vl-scopename-p first)
                              (vl-maybe-paramargs-p paramargs)
                              (vl-scopeexpr-p rest))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-scopeexpr-colon))
    (declare (ignorable __function__))
    (b* ((first (mbe :logic (vl-scopename-fix first)
                     :exec first))
         (paramargs (mbe :logic (vl-maybe-paramargs-fix paramargs)
                         :exec paramargs))
         (rest (mbe :logic (vl-scopeexpr-fix rest)
                    :exec rest)))
      (if paramargs
          (cons :paramscolon (cons first (cons paramargs rest)))
        (cons :colon (cons first rest))))))