		Search-engine friendly clone of the ACL2 documentation.

Fgl-env

Change-fgl-env

Modifying constructor for fgl-env structures.

Syntax

(change-fgl-env x 
                [:obj-alist <obj-alist>] 
                [:bfr-vals <bfr-vals>])

This is an often useful alternative to make-fgl-env.

We construct a new fgl-env 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-fgl-env

(defmacro change-fgl-env (x &rest args)
  (std::change-aggregate 'fgl-env
                         x args
                         '((:obj-alist . fgl-env->obj-alist)
                           (:bfr-vals . fgl-env->bfr-vals))
                         'change-fgl-env
                         'remake-fgl-env))