		Search-engine friendly clone of the ACL2 documentation.

Vl-tname

Make-vl-tname

Basic constructor macro for vl-tname structures.

Syntax

(make-vl-tname [:base <base>] 
               [:model <model>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-tname

(defmacro make-vl-tname (&rest args)
  (std::make-aggregate 'vl-tname
                       args '((:base) (:model))
                       'make-vl-tname
                       nil))

Function: vl-tname

(defun vl-tname (base model)
  (declare (xargs :guard (and (stringp base) (stringp model))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-tname))
    (declare (ignorable __function__))
    (b* ((base (mbe :logic (str-fix base) :exec base))
         (model (mbe :logic (str-fix model)
                     :exec model)))
      (cons :vl-tname (list (cons 'base base)
                            (cons 'model model))))))