		Search-engine friendly clone of the ACL2 documentation.

Jimport

Make-jimport

Basic constructor macro for jimport structures.

Syntax

(make-jimport [:static? <static?>] 
              [:target <target>])

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

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

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-jimport

(defmacro make-jimport (&rest args)
  (std::make-aggregate 'jimport
                       args '((:static?) (:target))
                       'make-jimport
                       nil))

Function: jimport

(defun jimport (static? target)
  (declare (xargs :guard (and (booleanp static?)
                              (stringp target))))
  (declare (xargs :guard t))
  (let ((__function__ 'jimport))
    (declare (ignorable __function__))
    (b* ((static? (mbe :logic (acl2::bool-fix static?)
                       :exec static?))
         (target (mbe :logic (str-fix target)
                      :exec target)))
      (list (cons 'static? static?)
            (cons 'target target)))))