REWRITE-DEFNS-LIST : ARGTYPEREWRITE-DEFNS-LIST is an argument type.
A list whose first element is one of NONE, EAGER, LAZY1 and DUAL,
and whose other (optional) elements are lists whose first element is
one of these four options and whose other elements are the names of
The first element is the default behaviour for rewriting definitions,
and the other lists are lists of exceptions to this default, with a
different behaviour specified.
NONE: do not rewrite this definition at all.
EAGER: rewrite all of these definitions, in one big step, as soon
LAZY1: rewrite these, one step at a time, when there are no more
EAGER rewrites to do.
DUAL: as LAZY1, but rewrite these abbreviations A to a conjunction of
A and A, and then deepen only one of these conjuncts. (e.g.
TRANSITIVE p becomes
TRANSITIVE p AND FORALL x y z . [pxy AND pyz] IMPLIES pxz
LAZY2: synonym for DUAL.
For example: the value
would be interpreted as "Rewrite every definition in one step."
(DUAL (EAGER TRANSITIVE) (NONE INJECTIVE SURJECTIVE))
would be interpreted as "Rewrite TRANSITIVE whenever it appears.
Don't ever rewrite INJECTIVE or SURJECTIVE. Rewrite every other
definition in the DUAL way."
TPS documentation homepage