`:`

`definition`

and `:`

`rewrite`

rules used in preprocessing
Major Section: MISCELLANEOUS

Example of simple rewrite rule: (equal (car (cons x y)) x) Examples of simple definition: (defun file-clock-p (x) (integerp x)) (defun naturalp (x) (and (integerp x) (>= x 0)))

The theorem prover output sometimes refers to ``simple'' definitions
and rewrite rules. These rules can be used by the preprocessor,
which is one of the theorem prover's ``processes'' understood by the
`:do-not`

hint; see hints.

The preprocessor expands certain definitions and uses certain
rewrite rules that it considers to be ``fast''. There are two ways
to qualify as fast. One is to be an ``abbreviation'', where a
rewrite rule with no hypotheses or loop stopper is an
``abbreviation'' if the right side contains no more variable
occurrences than the left side, and the right side does not call the
functions `if`

, `not`

or `implies`

. Definitions and rewrite rules can
both be abbreviations; the criterion for definitions is similar,
except that the definition must not be recursive. The other way to
qualify applies only to a non-recursive definition, and applies when
its body is a disjunction or conjunction, according to a perhaps
subtle criterion that is intended to avoid case splits.