		Search-engine friendly clone of the ACL2 documentation.

Meta-functions

Expand-member-meta

Meta function for member-equal.

This meta function is designed to quickly rewrite (MEMBER-EQUAL x l) to a set of nested IFs. This will happen if l is a EQLABLE-LISTP constant. Terms of this form arise for example in case macros.

Definitions and Theorems

Function: expand-member-meta

(defun expand-member-meta (term)
  (declare (xargs :guard (pseudo-termp term)))
  (case-match term
    (('member-equal x ('quote l))
     (if (eqlable-listp l)
         (formal-member x l)
       term))
    (& term)))

This meta rule rewrites (MEMBER-EQUAL x l) to a set of nested IFs. If l is an eqlable-listp constant, then we rewrite (MEMBER-EQUAL x l) to a set of nested IFs. This lemma is used for example to rewrite expressions generated by case macros for multiple choices, without the necessity of enableing member-equal and eqlable-listp.

Theorem: expand-member-meta-correct

(defthm expand-member-meta-correct
  (implies (and (pseudo-termp term) (alistp a))
           (equal (meta-ev term a)
                  (meta-ev (expand-member-meta term) a)))
  :rule-classes ((:meta :trigger-fns (member))))