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

definitions.

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

as possible.

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

(EAGER)

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."

© 1988-99, Carnegie Mellon University.