REWRITE-EQUALITIES : FLAG

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

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage