		Search-engine friendly clone of the ACL2 documentation.

Atc-fn-info

Change-atc-fn-info

Modifying constructor for atc-fn-info structures.

Syntax

(change-atc-fn-info x 
                    [:out-type <out-type>] 
                    [:in-types <in-types>] 
                    [:loop? <loop?>] 
                    [:affect <affect>] 
                    [:extobjs <extobjs>] 
                    [:result-thm <result-thm>] 
                    [:correct-thm <correct-thm>] 
                    [:correct-mod-thm <correct-mod-thm>] 
                    [:measure-nat-thm <measure-nat-thm>] 
                    [:fun-env-thm <fun-env-thm>] 
                    [:limit <limit>] 
                    [:guard <guard>])

This is an often useful alternative to make-atc-fn-info.

We construct a new atc-fn-info 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-atc-fn-info

(defmacro change-atc-fn-info (x &rest args)
  (std::change-aggregate
       'atc-fn-info
       x args
       '((:out-type . atc-fn-info->out-type)
         (:in-types . atc-fn-info->in-types)
         (:loop? . atc-fn-info->loop?)
         (:affect . atc-fn-info->affect)
         (:extobjs . atc-fn-info->extobjs)
         (:result-thm . atc-fn-info->result-thm)
         (:correct-thm . atc-fn-info->correct-thm)
         (:correct-mod-thm . atc-fn-info->correct-mod-thm)
         (:measure-nat-thm . atc-fn-info->measure-nat-thm)
         (:fun-env-thm . atc-fn-info->fun-env-thm)
         (:limit . atc-fn-info->limit)
         (:guard . atc-fn-info->guard))
       'change-atc-fn-info
       'nil))