		Search-engine friendly clone of the ACL2 documentation.

Congruence-rule

Change-congruence-rule

Modifying constructor for congruence-rule structures.

Syntax

(change-congruence-rule x 
                        [:equiv-req <equiv-req>] 
                        [:fn <fn>] 
                        [:arg-contexts <arg-contexts>] 
                        [:arity <arity>])

This is an often useful alternative to make-congruence-rule.

We construct a new congruence-rule 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-congruence-rule

(defmacro change-congruence-rule (x &rest args)
  (std::change-aggregate
       'congruence-rule
       x args
       '((:equiv-req . congruence-rule->equiv-req)
         (:fn . congruence-rule->fn)
         (:arg-contexts . congruence-rule->arg-contexts)
         (:arity . congruence-rule->arity))
       'change-congruence-rule
       'nil))