		Search-engine friendly clone of the ACL2 documentation.

Smtlink-hint

Change-smtlink-hint

Modifying constructor for smtlink-hint structures.

Syntax

(change-smtlink-hint x 
                     [:functions <functions>] 
                     [:hypotheses <hypotheses>] 
                     [:main-hint <main-hint>] 
                     [:let-binding <let-binding>] 
                     [:symbols <symbols>] 
                     [:abs <abs>] 
                     [:fty <fty>] 
                     [:fty-info <fty-info>] 
                     [:fty-types <fty-types>] 
                     [:int-to-rat <int-to-rat>] 
                     [:smt-dir <smt-dir>] 
                     [:rm-file <rm-file>] 
                     [:smt-fname <smt-fname>] 
                     [:smt-params <smt-params>] 
                     [:fast-functions <fast-functions>] 
                     [:type-decl-list <type-decl-list>] 
                     [:expanded-clause-w/-hint <expanded-clause-w/-hint>] 
                     [:expanded-g/type <expanded-g/type>] 
                     [:smt-cnf <smt-cnf>] 
                     [:wrld-fn-len <wrld-fn-len>] 
                     [:custom-p <custom-p>])

This is an often useful alternative to make-smtlink-hint.

We construct a new smtlink-hint 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 defprod.

Macro: change-smtlink-hint

(defmacro change-smtlink-hint (x &rest args)
  (std::change-aggregate
       'smtlink-hint
       x args
       '((:functions . smtlink-hint->functions)
         (:hypotheses . smtlink-hint->hypotheses)
         (:main-hint . smtlink-hint->main-hint)
         (:let-binding . smtlink-hint->let-binding)
         (:symbols . smtlink-hint->symbols)
         (:abs . smtlink-hint->abs)
         (:fty . smtlink-hint->fty)
         (:fty-info . smtlink-hint->fty-info)
         (:fty-types . smtlink-hint->fty-types)
         (:int-to-rat . smtlink-hint->int-to-rat)
         (:smt-dir . smtlink-hint->smt-dir)
         (:rm-file . smtlink-hint->rm-file)
         (:smt-fname . smtlink-hint->smt-fname)
         (:smt-params . smtlink-hint->smt-params)
         (:fast-functions . smtlink-hint->fast-functions)
         (:type-decl-list . smtlink-hint->type-decl-list)
         (:expanded-clause-w/-hint
              . smtlink-hint->expanded-clause-w/-hint)
         (:expanded-g/type . smtlink-hint->expanded-g/type)
         (:smt-cnf . smtlink-hint->smt-cnf)
         (:wrld-fn-len . smtlink-hint->wrld-fn-len)
         (:custom-p . smtlink-hint->custom-p))
       'change-smtlink-hint
       'nil))