		Search-engine friendly clone of the ACL2 documentation.

Snippet-info

Change-snippet-info

Modifying constructor for snippet-info structures.

Syntax

(change-snippet-info x 
                     [:name <name>] 
                     [:input-size <input-size>] 
                     [:output-size <output-size>] 
                     [:addr <addr>])

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

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

(defmacro change-snippet-info (x &rest args)
 (std::change-aggregate 'snippet-info
                        x args
                        '((:name . snippet-info->name)
                          (:input-size . snippet-info->input-size)
                          (:output-size . snippet-info->output-size)
                          (:addr . snippet-info->addr))
                        'change-snippet-info
                        'nil))