		Search-engine friendly clone of the ACL2 documentation.

Deffixequiv

Fixequiv-hook

An std::post-define-hook for automatically proving fty congruences rules.

The :fix hook allows you to instruct define to automatically try to infer and prove appropriate congruence rules as in deffixequiv.

Typical usage, to try to automatically prove congruences everywhere, is to simply add the following to the top of your file, section, encapsulate, or similar:

(local (std::add-default-post-define-hook :fix))

You will almost certainly want to ensure that this is done locally, since otherwise it will affect all users who include your book.

For finer-grained control or to suppress equivalences for a particular function, you can use the :hooks argument to an individual define, e.g.,

(define none ((n natp))    ;; don't prove any congruences
   :hooks nil
   n)

(define custom ((a natp) (b natp))   ;; prove congruences only
   :hooks ((:fix :omit (b)))         ;; for A, not for B
   (list (nfix a) b))

(define custom2 ((a natp) (b natp))       ;; prove congruences other than
   :hooks ((:fix :args ((a integerp)      ;; those the formals suggest
                        (b rationalp))))
   (list (ifix a) (rfix b)))

The arguments beyond :fix get passed to deffixequiv, so see its documentation for more options.