		Search-engine friendly clone of the ACL2 documentation.

Defstruct-info

Change-defstruct-info

Modifying constructor for defstruct-info structures.

Syntax

(change-defstruct-info x 
                       [:tag <tag>] 
                       [:members <members>] 
                       [:flexiblep <flexiblep>] 
                       [:fixtype <fixtype>] 
                       [:recognizer <recognizer>] 
                       [:fixer <fixer>] 
                       [:fixer-recognizer-thm <fixer-recognizer-thm>] 
                       [:not-error-thm <not-error-thm>] 
                       [:valuep-thm <valuep-thm>] 
                       [:value-kind-thm <value-kind-thm>] 
                       [:type-of-value-thm <type-of-value-thm>] 
                       [:flexiblep-thm <flexiblep-thm>] 
                       [:type-to-quoted-thm <type-to-quoted-thm>] 
                       [:pointer-type-to-quoted-thm <pointer-type-to-quoted-thm>] 
                       [:call <call>])

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

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

(defmacro change-defstruct-info (x &rest args)
 (std::change-aggregate
    'defstruct-info
    x args
    '((:tag . defstruct-info->tag)
      (:members . defstruct-info->members)
      (:flexiblep . defstruct-info->flexiblep)
      (:fixtype . defstruct-info->fixtype)
      (:recognizer . defstruct-info->recognizer)
      (:fixer . defstruct-info->fixer)
      (:fixer-recognizer-thm . defstruct-info->fixer-recognizer-thm)
      (:not-error-thm . defstruct-info->not-error-thm)
      (:valuep-thm . defstruct-info->valuep-thm)
      (:value-kind-thm . defstruct-info->value-kind-thm)
      (:type-of-value-thm . defstruct-info->type-of-value-thm)
      (:flexiblep-thm . defstruct-info->flexiblep-thm)
      (:type-to-quoted-thm . defstruct-info->type-to-quoted-thm)
      (:pointer-type-to-quoted-thm
           .
           defstruct-info->pointer-type-to-quoted-thm)
      (:call . defstruct-info->call))
    'change-defstruct-info
    'nil))