		Search-engine friendly clone of the ACL2 documentation.

Vl-zipinfo

Make-vl-zipinfo

Basic constructor macro for vl-zipinfo structures.

Syntax

(make-vl-zipinfo [:filename <filename>] 
                 [:name <name>] 
                 [:syntax <syntax>] 
                 [:date <date>] 
                 [:ltime <ltime>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-zipinfo

(defmacro make-vl-zipinfo (&rest args)
  (std::make-aggregate 'vl-zipinfo
                       args
                       '((:filename)
                         (:name)
                         (:syntax)
                         (:date)
                         (:ltime))
                       'make-vl-zipinfo
                       nil))

Function: vl-zipinfo

(defun vl-zipinfo (filename name syntax date ltime)
  (declare (xargs :guard (and (stringp filename)
                              (stringp name)
                              (stringp syntax)
                              (stringp date)
                              (natp ltime))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-zipinfo))
    (declare (ignorable __function__))
    (b* ((filename (mbe :logic (str-fix filename)
                        :exec filename))
         (name (mbe :logic (str-fix name) :exec name))
         (syntax (mbe :logic (str-fix syntax)
                      :exec syntax))
         (date (mbe :logic (str-fix date) :exec date))
         (ltime (mbe :logic (nfix ltime) :exec ltime)))
      (cons :vl-zipinfo (list (cons 'filename filename)
                              (cons 'name name)
                              (cons 'syntax syntax)
                              (cons 'date date)
                              (cons 'ltime ltime))))))