		Search-engine friendly clone of the ACL2 documentation.

Hint-pair

Change-hint-pair

Modifying constructor for hint-pair structures.

Syntax

(change-hint-pair x 
                  [:thm <thm>] 
                  [:hints <hints>])

This is an often useful alternative to make-hint-pair.

We construct a new hint-pair 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 defprod.

Macro: change-hint-pair

(defmacro change-hint-pair (x &rest args)
  (std::change-aggregate 'hint-pair
                         x args
                         '((:thm . hint-pair->thm)
                           (:hints . hint-pair->hints))
                         'change-hint-pair
                         'nil))