Conventional-normal-forms
Recommendations for respecting global conventions that the ACL2 books
authors have agreed to.
In many cases there are alternate normal forms that you can use for
the same concept. For greater compatibility between libraries, we prefer to
use various forms as described below.
Recommendations:
- Write lemmas in terms of (mv-nth n ...) instead of (caddr ...)
- Include the tools/mv-nth book
Rationale
- It's important to have a standard here since multiply-valued functions
are needed in many libraries.
- Leaving mv-nth enabled is worse because it leads to different normal
forms for slot 0 versus other slots. That is, ACL2 will rewrite (mv-nth 0
...) to (car ...) but will not rewrite (mv-nth 1 ...) unless
additional rewrite rules are added.
- Writing theorems in terms of mv-nth is compatible with using b*
bindings in theorems, which is particularly nice.
BOZO Other important normal forms we should all agree on?
Member versus Memberp?
