		Search-engine friendly clone of the ACL2 documentation.

Section-info

Change-section-info

Modifying constructor for section-info structures.

Syntax

(change-section-info x 
                     [:header <header>] 
                     [:bytes <bytes>])

This is an often useful alternative to make-section-info.

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

(defmacro change-section-info (x &rest args)
  (std::change-aggregate 'section-info
                         x args
                         '((:header . section-info->header)
                           (:bytes . section-info->bytes))
                         'change-section-info
                         'nil))