		Search-engine friendly clone of the ACL2 documentation.

Constants-conversions-and-bounds

Np-defs

Signature
(np-defs lst) → *

Definitions and Theorems

Function: np-defs

(defun np-defs (lst)
  (declare (xargs :guard (acl2::pos-listp lst)))
  (let ((__function__ 'np-defs))
    (declare (ignorable __function__))
    (if (atom lst)
        nil
      (append (np-def-n (car lst))
              (np-defs (cdr lst))))))