		Search-engine friendly clone of the ACL2 documentation.

Fact-infop

Change-fact-info

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

Syntax:

(change-fact-info x 
                  [:thm-name <thm-name>] 
                  [:formula <formula>])

This is a sometimes useful alternative to make-fact-info. It constructs a new fact-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-fact-info

(defmacro change-fact-info (x &rest args)
  (std::change-aggregate 'fact-info
                         x args
                         '((:thm-name . fact-info->thm-name)
                           (:formula . fact-info->formula))
                         'change-fact-info
                         'nil))