		Search-engine friendly clone of the ACL2 documentation.

Observability-config

Change-observability-config

Modifying constructor for observability-config structures.

Syntax

(change-observability-config x 
                             [:hyp-max-size <hyp-max-size>] 
                             [:concl-min-size <concl-min-size>] 
                             [:min-ratio <min-ratio>] 
                             [:gatesimp <gatesimp>])

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

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

(defmacro change-observability-config (x &rest args)
  (std::change-aggregate
       'observability-config
       x args
       '((:hyp-max-size . observability-config->hyp-max-size)
         (:concl-min-size . observability-config->concl-min-size)
         (:min-ratio . observability-config->min-ratio)
         (:gatesimp . observability-config->gatesimp))
       'change-observability-config
       'nil))