		Search-engine friendly clone of the ACL2 documentation.

Dec-expo

Change-dec-expo

Modifying constructor for dec-expo structures.

Syntax

(change-dec-expo x 
                 [:prefix <prefix>] 
                 [:sign? <sign?>] 
                 [:digits <digits>])

This is an often useful alternative to make-dec-expo.

We construct a new dec-expo 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 fty::defprod.

Macro: change-dec-expo

(defmacro change-dec-expo (x &rest args)
  (std::change-aggregate 'dec-expo
                         x args
                         '((:prefix . dec-expo->prefix)
                           (:sign? . dec-expo->sign?)
                           (:digits . dec-expo->digits))
                         'change-dec-expo
                         'nil))