### NOTE-2-8-RULES

ACL2 Version 2.8 Notes on Changes in Rules, Definitions, and Constants
Major Section: NOTE-2-8

The theory `minimal-theory`

has been changed by adding the
definition rune for `mv-nth`

to the theory. A corresponding
change has been made to the theory warning mechanism, which was failing to
warn if the definition of `mv-nth`

is disabled, even though calls of
`mv-nth`

can be expanded by special-purpose code in the rewriter. Thanks
to Serita Van Groningen for pointing out this problem with the theory warning
mechanism.

The `defevaluator`

event has been modified so that in the body of the
evaluator function, to add a new case `(ATOM X)`

(returning `nil`

) has
been inserted immediately after the case `(EQ (CAR X) 'QUOTE)`

. This is a
no-op semantically but may speed up proofs. Thanks to Warren Hunt for
suggesting this change.

A new form of `:`

`compound-recognizer`

rule is now allowed:

(if (fn x) concl1 concl2)

This is equivalent to an existing form:
(and (implies (fn x) concl1)
(implies (not (fn x)) concl2))

Thanks to Josh Purinton for bringing this to our attention.
Rewrite rules `realpart-+`

and `imagpart-+`

have been added in order
to simplify the `realpart`

and `imagpart`

(respectively) of a sum.
They follow from a theorem `add-def-complex`

that equates a sum with
the complex number formed by adding real and imaginary parts. All three
of these theorems may be found in source file `axioms.lisp`

. Thanks to
Eric Smith for raising a question leading to these additions, as well as
to Joe Hendrix and Vernon Austel for helpful suggestions.