		Search-engine friendly clone of the ACL2 documentation.

Run-snippet-file-info

Change-run-snippet-file-info

Modifying constructor for run-snippet-file-info structures.

Syntax

(change-run-snippet-file-info x 
                              [:snip-info <snip-info>] 
                              [:input-addr <input-addr>] 
                              [:output-addr <output-addr>] 
                              [:input-channel <input-channel>] 
                              [:output-channel <output-channel>])

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

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

(defmacro change-run-snippet-file-info (x &rest args)
  (std::change-aggregate
       'run-snippet-file-info
       x args
       '((:snip-info . run-snippet-file-info->snip-info)
         (:input-addr . run-snippet-file-info->input-addr)
         (:output-addr . run-snippet-file-info->output-addr)
         (:input-channel . run-snippet-file-info->input-channel)
         (:output-channel .
                          run-snippet-file-info->output-channel))
       'change-run-snippet-file-info
       'nil))