		Search-engine friendly clone of the ACL2 documentation.

Defobject-info

Change-defobject-info

Modifying constructor for defobject-info structures.

Syntax

(change-defobject-info x 
                       [:name-ident <name-ident>] 
                       [:name-symbol <name-symbol>] 
                       [:type <type>] 
                       [:init <init>] 
                       [:recognizer <recognizer>] 
                       [:initializer <initializer>] 
                       [:call <call>])

This is an often useful alternative to make-defobject-info.

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

(defmacro change-defobject-info (x &rest args)
  (std::change-aggregate
       'defobject-info
       x args
       '((:name-ident . defobject-info->name-ident)
         (:name-symbol . defobject-info->name-symbol)
         (:type . defobject-info->type)
         (:init . defobject-info->init)
         (:recognizer . defobject-info->recognizer)
         (:initializer . defobject-info->initializer)
         (:call . defobject-info->call))
       'change-defobject-info
       'nil))