		Search-engine friendly clone of the ACL2 documentation.

Sponge

Change-sponge

Modifying constructor for sponge structures.

Syntax

(change-sponge x 
               [:stat <stat>] 
               [:mode <mode>] 
               [:index <index>])

This is an often useful alternative to make-sponge.

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

(defmacro change-sponge (x &rest args)
  (std::change-aggregate 'sponge
                         x args
                         '((:stat . sponge->stat)
                           (:mode . sponge->mode)
                           (:index . sponge->index))
                         'change-sponge
                         'nil))