		Search-engine friendly clone of the ACL2 documentation.

Fhg-single-args

Change-fhg-single-args

Modifying constructor for fhg-single-args structures.

Syntax

(change-fhg-single-args x 
                        [:fn <fn>] 
                        [:actuals <actuals>] 
                        [:fn-returns-hint-acc <fn-returns-hint-acc>] 
                        [:fn-more-returns-hint-acc <fn-more-returns-hint-acc>] 
                        [:lambda-acc <lambda-acc>])

This is an often useful alternative to make-fhg-single-args.

We construct a new fhg-single-args 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-fhg-single-args

(defmacro change-fhg-single-args (x &rest args)
 (std::change-aggregate
     'fhg-single-args
     x args
     '((:fn . fhg-single-args->fn)
       (:actuals . fhg-single-args->actuals)
       (:fn-returns-hint-acc . fhg-single-args->fn-returns-hint-acc)
       (:fn-more-returns-hint-acc
            .
            fhg-single-args->fn-more-returns-hint-acc)
       (:lambda-acc . fhg-single-args->lambda-acc))
     'change-fhg-single-args
     'nil))