REWRITE-DEFNS : ARGTYPE

REWRITE-DEFNS is an argument type.
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.

TPS documentation homepage


REWRITE-DEFNS : FLAG

REWRITE-DEFNS is a flag or parameter.
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).

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage