		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Toplevel-fn-names

Signature
(toplevel-fn-names top) → nms
Arguments: top — Guard (toplevelp top).
Returns: nms — Type (string-listp nms).

Definitions and Theorems

Function: toplevel-fn-names

(defun toplevel-fn-names (top)
  (declare (xargs :guard (toplevelp top)))
  (let ((__function__ 'toplevel-fn-names))
    (declare (ignorable __function__))
    (if (toplevelp top)
        (case (toplevel-kind top)
          (:function (function-definition-names
                          (list (toplevel-function->get top))))
          (:functions (function-definition-names
                           (function-recursion->definitions
                                (toplevel-functions->get top))))
          (otherwise nil))
      nil)))

Theorem: string-listp-of-toplevel-fn-names

(defthm string-listp-of-toplevel-fn-names
  (b* ((nms (toplevel-fn-names top)))
    (string-listp nms))
  :rule-classes :rewrite)