		Search-engine friendly clone of the ACL2 documentation.

Parametrize-config

Change-parametrize-config

Modifying constructor for parametrize-config structures.

Syntax

(change-parametrize-config x 
                           [:build-limit <build-limit>] 
                           [:conjoin-limit <conjoin-limit>] 
                           [:output-types <output-types>])

This is an often useful alternative to make-parametrize-config.

We construct a new parametrize-config 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-parametrize-config

(defmacro change-parametrize-config (x &rest args)
  (std::change-aggregate
       'parametrize-config
       x args
       '((:build-limit . parametrize-config->build-limit)
         (:conjoin-limit . parametrize-config->conjoin-limit)
         (:output-types . parametrize-config->output-types))
       'change-parametrize-config
       'nil))