		Search-engine friendly clone of the ACL2 documentation.

Vl-timeliteral

Make-vl-timeliteral

Basic constructor macro for vl-timeliteral structures.

Syntax

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

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-timeliteral

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

Function: vl-timeliteral

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