One of the following:

NONE: do not rewrite equalities

ONLY-EXT: rewrite only those equalities that can be rewritten using

extensionality.

LEIBNIZ: rewrite all equalities using the Leibniz definition.

ALL: rewrite all equalities, using extensionality where possible

and the Leibniz definition otherwise.

DUAL: As in the flag REWRITE-DEFNS.

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

REWRITE-DEFNS takes values of type REWRITE-DEFNS-LIST.

It belongs to subjects MS98-1 MS93-1 MS92-9 MS91-7 MS91-6 MS90-9 MS90-3 MS89 MS88 IMPORTANT MATING-SEARCH .

Its default value is (EAGER)

Its current value is (EAGER).

© 1988-99, Carnegie Mellon University.