		Search-engine friendly clone of the ACL2 documentation.

Bexpo

Change-bexpo

Modifying constructor for bexpo structures.

Syntax

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

This is an often useful alternative to make-bexpo.

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

(defmacro change-bexpo (x &rest args)
  (std::change-aggregate 'bexpo
                         x args
                         '((:prefix . bexpo->prefix)
                           (:sign? . bexpo->sign?)
                           (:digits . bexpo->digits))
                         'change-bexpo
                         'remake-bexpo))