		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Nrec-list-mods

Signature
(nrec-list-mods keys moddb) → *

Definitions and Theorems

Function: nrec-list-mods

(defun nrec-list-mods (keys moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :non-executable t))
  (declare (xargs :guard t))
  (prog2$ (acl2::throw-nonexec-error 'nrec-list-mods
                                     (list keys moddb))
          (let ((__function__ 'nrec-list-mods))
            (declare (ignorable __function__))
            (update-nth *moddb->modsi*
                        (nrec-list keys (nth *moddb->modsi* moddb))
                        moddb))))