		Search-engine friendly clone of the ACL2 documentation.

Vl-time

Make-vl-time

Basic constructor macro for vl-time structures.

Syntax

(make-vl-time [:quantity <quantity>] 
              [:units <units>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-time

(defmacro make-vl-time (&rest args)
  (std::make-aggregate 'vl-time
                       args '((:quantity) (:units))
                       'make-vl-time
                       nil))

Function: vl-time

(defun vl-time (quantity units)
  (declare (xargs :guard (and (stringp quantity)
                              (vl-timeunit-p units))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-time))
    (declare (ignorable __function__))
    (b* ((quantity (mbe :logic (str-fix quantity)
                        :exec quantity))
         (units (mbe :logic (vl-timeunit-fix units)
                     :exec units)))
      (hons :vl-time (std::prod-hons quantity units)))))