		Search-engine friendly clone of the ACL2 documentation.

Execution-environmentp

Change-execution-environment

A copying macro that lets you create new execution-environmentp structures, based on existing structures.

Syntax:

(change-execution-environment x 
                              [:owner-address <owner-address>] 
                              [:sender-address <sender-address>] 
                              [:gas-price <gas-price>] 
                              [:input-data <input-data>] 
                              [:causer-account <causer-account>] 
                              [:value <value>] 
                              [:bytecode <bytecode>] 
                              [:block-header <block-header>] 
                              [:depth <depth>] 
                              [:permission <permission>])

This is a sometimes useful alternative to make-execution-environment. It constructs a new execution-environmentp 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-execution-environment

(defmacro change-execution-environment (x &rest args)
  (std::change-aggregate
       'execution-environment
       x args
       '((:owner-address . execution-environment->owner-address)
         (:sender-address . execution-environment->sender-address)
         (:gas-price . execution-environment->gas-price)
         (:input-data . execution-environment->input-data)
         (:causer-account . execution-environment->causer-account)
         (:value . execution-environment->value)
         (:bytecode . execution-environment->bytecode)
         (:block-header . execution-environment->block-header)
         (:depth . execution-environment->depth)
         (:permission . execution-environment->permission))
       'change-execution-environment
       'nil))