		Search-engine friendly clone of the ACL2 documentation.

Chase-position

Change-chase-position

Modifying constructor for chase-position structures.

Syntax

(change-chase-position x 
                       [:path <path>] 
                       [:phase <phase>] 
                       [:rsh <rsh>] 
                       [:mask <mask>])

This is an often useful alternative to make-chase-position.

We construct a new chase-position 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-chase-position

(defmacro change-chase-position (x &rest args)
  (std::change-aggregate 'chase-position
                         x args
                         '((:path . chase-position->path)
                           (:phase . chase-position->phase)
                           (:rsh . chase-position->rsh)
                           (:mask . chase-position->mask))
                         'change-chase-position
                         'nil))