data-structures/alist-defthms and coi/alists/ are incompatible

[ragerdl]

data-structures/alist-defthms and coi/alists/ are incompatible

[ragerdl]

From [email protected] on May 10, 2011 17:10:51

Hi --

Good points.

The two theorems mentioned have already been
eliminated from the trunk, in anticipation of a
change made for the next release (4.3) of ACL2
(because those lemmas will no longer be necessary
or useful). Starting with that release, assoc and
assoc-equal will essentially be the same from a
logical perspective. Below is the (Emacs Info
version of) the paragraph about this from the
upcoming :doc note-4-3. If you or anyone wants to
make some changes to the regression suite along
the lines that you suggested, feel free to contact
me about getting a development snapshot of ACL2.

Significant changes have been made for
list-processing primitives such as member and
assoc; see *note EQUALITY-VARIANTS::. In
summary: instead of separate functions based on
eq, eql, and equal, there is essentially just
one function, which is based on equal; the eq
and eql variants are logically just the equal
variant. For example, member-eq and member are
macros that generate corresponding calls of
member-equal in the logic, although in raw Lisp
they will execute using tests eq and eql,
respectively. References to any of these in
logical contexts such as theories are now
references to the function based on equal; for
example, the hint :in-theory (disable member) is
completely equivalent to the hint :in-theory
(disable member-equal). Distributed books have
been modified as necessary to accommodate this
change. While the need for such changes was
relatively infrequent, changes were for example
needed in contexts where terms are manipulated
directly; for example, defevaluator needs to
mention member-equal rather than member, just as
it was already the case to mention, say,
binary-append rather than append. Again, see
*note EQUALITY-VARIANTS:: for more information
about equality variants.

Regards,
Matt

[ragerdl]

From [email protected] on February 27, 2013 16:52:36

Status: Fixed

[ragerdl]

From [email protected] on September 03, 2014 04:55:48

Labels: Type-Enhancement