		Search-engine friendly clone of the ACL2 documentation.

Jcinitializer

Make-jcinitializer

Basic constructor macro for jcinitializer structures.

Syntax

(make-jcinitializer [:static? <static?>] 
                    [:code <code>])

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

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

Definition

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

Macro: make-jcinitializer

(defmacro make-jcinitializer (&rest args)
  (std::make-aggregate 'jcinitializer
                       args '((:static?) (:code))
                       'make-jcinitializer
                       nil))

Function: jcinitializer

(defun jcinitializer (static? code)
  (declare (xargs :guard (and (booleanp static?)
                              (jblockp code))))
  (declare (xargs :guard t))
  (let ((__function__ 'jcinitializer))
    (declare (ignorable __function__))
    (b* ((static? (mbe :logic (acl2::bool-fix static?)
                       :exec static?))
         (code (mbe :logic (jblock-fix code)
                    :exec code)))
      (list (cons 'static? static?)
            (cons 'code code)))))