		Search-engine friendly clone of the ACL2 documentation.

Constraint-tuple

Change-constraint-tuple

Modifying constructor for constraint-tuple structures.

Syntax

(change-constraint-tuple x 
                         [:rule <rule>] 
                         [:existing-lits <existing-lits>] 
                         [:matching-lit <matching-lit>] 
                         [:common-vars <common-vars>] 
                         [:existing-vars <existing-vars>] 
                         [:sig-table <sig-table>])

This is an often useful alternative to make-constraint-tuple.

We construct a new constraint-tuple 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-constraint-tuple

(defmacro change-constraint-tuple (x &rest args)
  (std::change-aggregate
       'constraint-tuple
       x args
       '((:rule . constraint-tuple->rule)
         (:existing-lits . constraint-tuple->existing-lits)
         (:matching-lit . constraint-tuple->matching-lit)
         (:common-vars . constraint-tuple->common-vars)
         (:existing-vars . constraint-tuple->existing-vars)
         (:sig-table . constraint-tuple->sig-table))
       'change-constraint-tuple
       'remake-constraint-tuple))