		Search-engine friendly clone of the ACL2 documentation.

Vl-cast

Make-vl-cast

Basic constructor macro for vl-cast structures.

Syntax

(make-vl-cast [:to <to>] 
              [:expr <expr>] 
              [:atts <atts>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-cast

(defmacro make-vl-cast (&rest args)
  (std::make-aggregate 'vl-cast
                       args '((:to) (:expr) (:atts))
                       'make-vl-cast
                       nil))

Function: vl-cast

(defun vl-cast (to expr atts)
 (declare (xargs :guard (and (vl-casttype-p to)
                             (vl-expr-p expr)
                             (vl-atts-p atts))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-cast))
  (declare (ignorable __function__))
  (b* ((to (mbe :logic (vl-casttype-fix to)
                :exec to))
       (expr (mbe :logic (vl-expr-fix expr)
                  :exec expr))
       (atts (mbe :logic (vl-atts-fix atts)
                  :exec atts)))
   (cons :vl-cast (std::prod-cons to (std::prod-cons expr atts))))))