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, to an equivalence for those of type OOO,

to the extensional form

[lambda f(AB) lambda g(AB) forall x(B) f x = g x]

for those of type O(AB)(AB), and to the Leibniz form

[lambda x(A) lambda y(A) forall q(OA). q x implies q y]

for those of type OAA.

LAZY2: As for ALL, but keeping a duplicate leaf as in the LAZY2

setting of the flag REWRITE-DEFNS.

REWRITE-EQUALITIES takes values of type REWRITE-DEFNS.

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

Its default value is ALL

Its current value is ALL.

© 1988-99, Carnegie Mellon University.