		Search-engine friendly clone of the ACL2 documentation.

Run-snippet-info

Change-run-snippet-info

Modifying constructor for run-snippet-info structures.

Syntax

(change-run-snippet-info x 
                         [:input-size <input-size>] 
                         [:output-size <output-size>] 
                         [:snip-addr <snip-addr>] 
                         [:ret-addr <ret-addr>] 
                         [:step-count <step-count>])

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

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

(defmacro change-run-snippet-info (x &rest args)
  (std::change-aggregate
       'run-snippet-info
       x args
       '((:input-size . run-snippet-info->input-size)
         (:output-size . run-snippet-info->output-size)
         (:snip-addr . run-snippet-info->snip-addr)
         (:ret-addr . run-snippet-info->ret-addr)
         (:step-count . run-snippet-info->step-count))
       'change-run-snippet-info
       'nil))