		Search-engine friendly clone of the ACL2 documentation.

Meta-functions

Reduce-nth-meta

Meta function for nth.

This meta function is designed to quickly rewrite terms of the form (NTH n lst) where n is an integer and lst is formally a proper list.

Definitions and Theorems

Function: reduce-nth-meta

(defun reduce-nth-meta (term)
  (declare (xargs :guard (pseudo-termp term)))
  (case-match term
    (('nth ('quote n) lst)
     (if (and (integerp n)
              (<= 0 n)
              (equal (formal-true-listp lst) *t*))
         (formal-nth n lst)
       term))
    (& term)))

This meta lemma was designed to quickly rewrite the terms generated by the mv-let macro.

Theorem: reduce-nth-meta-correct

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