An std::post-define-hook for automatically proving fty congruences rules.
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
(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