		Search-engine friendly clone of the ACL2 documentation.

Jcinitializer

Change-jcinitializer

Modifying constructor for jcinitializer structures.

Syntax

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

This is an often useful alternative to make-jcinitializer.

We construct a new jcinitializer structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

Definition

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

Macro: change-jcinitializer

(defmacro change-jcinitializer (x &rest args)
  (std::change-aggregate 'jcinitializer
                         x args
                         '((:static? . jcinitializer->static?)
                           (:code . jcinitializer->code))
                         'change-jcinitializer
                         'nil))