		Search-engine friendly clone of the ACL2 documentation.

Te-args

Change-te-args

Modifying constructor for te-args structures.

Syntax

(change-te-args x 
                [:expr-lst <expr-lst>] 
                [:fn-lst <fn-lst>] 
                [:fty-info <fty-info>] 
                [:symbol-index <symbol-index>] 
                [:symbol-list <symbol-list>] 
                [:avoid-list <avoid-list>] 
                [:symbol-map <symbol-map>])

This is an often useful alternative to make-te-args.

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

(defmacro change-te-args (x &rest args)
  (std::change-aggregate 'te-args
                         x args
                         '((:expr-lst . te-args->expr-lst)
                           (:fn-lst . te-args->fn-lst)
                           (:fty-info . te-args->fty-info)
                           (:symbol-index . te-args->symbol-index)
                           (:symbol-list . te-args->symbol-list)
                           (:avoid-list . te-args->avoid-list)
                           (:symbol-map . te-args->symbol-map))
                         'change-te-args
                         'nil))