ELIM-DEFNS is a flag or parameter.
When printing a wff, first instantiate all of the definitions
and lambda-normalize. This instantiation will ignore REWRITE-DEFNS, but
will use the current setting of REWRITE-EQUALITIES.
It's best to leave this at NIL (i.e. off), since output with it set to T can
be confusing.
ELIM-DEFNS takes values of type BOOLEAN.
It belongs to subjects LIBRARY PRINTING .
Its default value is NIL
Its current value is NIL.

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage