		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb->nmods

Signature
(moddb->nmods moddb) → *

Definitions and Theorems

Function: moddb->nmods$inline

(defun moddb->nmods$inline (moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard t))
  (let ((__function__ 'moddb->nmods))
    (declare (ignorable __function__))
    (mbe :logic (non-exec (nfix (nth *moddb->nmods* moddb)))
         :exec (moddb->nmods1 moddb))))