		Search-engine friendly clone of the ACL2 documentation.

Sparseint$-concat

Change-sparseint$-concat

Modifying constructor for sparseint$-concat structures.

Syntax

(change-sparseint$-concat x 
                          [:width <width>] 
                          [:lsbs-taller <lsbs-taller>] 
                          [:msbs-taller <msbs-taller>] 
                          [:lsbs <lsbs>] 
                          [:msbs <msbs>])

This is an often useful alternative to make-sparseint$-concat.

We construct a new sparseint$-concat 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-sparseint$-concat

(defmacro change-sparseint$-concat (x &rest args)
  (std::change-aggregate
       'sparseint$-concat
       x args
       '((:width . sparseint$-concat->width)
         (:lsbs-taller . sparseint$-concat->lsbs-taller)
         (:msbs-taller . sparseint$-concat->msbs-taller)
         (:lsbs . sparseint$-concat->lsbs)
         (:msbs . sparseint$-concat->msbs))
       'change-sparseint$-concat
       'nil))