		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Nrec-list

Signature
(nrec-list keys rs) → *

Definitions and Theorems

Function: nrec-list

(defun nrec-list (keys rs)
  (declare (xargs :guard t))
  (let ((__function__ 'nrec-list))
    (declare (ignorable __function__))
    (if (atom rs)
        nil
      (cons (nrec keys (car rs))
            (nrec-list keys (cdr rs))))))