		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-infop

Change-defarbrec-info

A copying macro that lets you create new defarbrec-infop structures, based on existing structures.

Syntax:

(change-defarbrec-info x 
                       [:call$ <call$>] 
                       [:expansion <expansion>] 
                       [:x1...xn <x1...xn>] 
                       [:body <body>] 
                       [:update-fns <update-fns>] 
                       [:terminates-fn <terminates-fn>] 
                       [:measure-fn <measure-fn>])

This is a sometimes useful alternative to make-defarbrec-info. It constructs a new defarbrec-infop 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 std::defaggregate.

Macro: change-defarbrec-info

(defmacro change-defarbrec-info (x &rest args)
  (std::change-aggregate
       'defarbrec-info
       x args
       '((:call$ . defarbrec-info->call$)
         (:expansion . defarbrec-info->expansion)
         (:x1...xn . defarbrec-info->x1...xn)
         (:body . defarbrec-info->body)
         (:update-fns . defarbrec-info->update-fns)
         (:terminates-fn . defarbrec-info->terminates-fn)
         (:measure-fn . defarbrec-info->measure-fn))
       'change-defarbrec-info
       'nil))