		Search-engine friendly clone of the ACL2 documentation.

Definterface-hmac-infop

Change-definterface-hmac-info

A copying macro that lets you create new definterface-hmac-infop structures, based on existing structures.

Syntax:

(change-definterface-hmac-info x 
                               [:key-size-limit <key-size-limit>] 
                               [:block-size <block-size>] 
                               [:output-size <output-size>])

This is a sometimes useful alternative to make-definterface-hmac-info. It constructs a new definterface-hmac-infop 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 std::defaggregate.

Macro: change-definterface-hmac-info

(defmacro change-definterface-hmac-info (x &rest args)
  (std::change-aggregate
       'definterface-hmac-info
       x args
       '((:key-size-limit .
                          definterface-hmac-info->key-size-limit)
         (:block-size . definterface-hmac-info->block-size)
         (:output-size . definterface-hmac-info->output-size))
       'change-definterface-hmac-info
       'nil))