		Search-engine friendly clone of the ACL2 documentation.

Finalization

Change-finalization

Modifying constructor for finalization structures.

Syntax

(change-finalization x 
                     [:command <command>] 
                     [:finalizer <finalizer>])

This is an often useful alternative to make-finalization.

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

(defmacro change-finalization (x &rest args)
  (std::change-aggregate 'finalization
                         x args
                         '((:command . finalization->command)
                           (:finalizer . finalization->finalizer))
                         'change-finalization
                         'nil))