		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Function-definition-names

Signature
(function-definition-names fns) → nms
Arguments: fns — Guard (function-definition-listp fns).
Returns: nms — Type (string-listp nms).

Definitions and Theorems

Function: function-definition-names

(defun function-definition-names (fns)
 (declare (xargs :guard (function-definition-listp fns)))
 (let ((__function__ 'function-definition-names))
  (declare (ignorable __function__))
  (if (endp fns)
      nil
   (cons
    (identifier->name (function-header->name
                           (function-definition->header (car fns))))
    (function-definition-names (cdr fns))))))

Theorem: string-listp-of-function-definition-names

(defthm string-listp-of-function-definition-names
  (b* ((nms (function-definition-names fns)))
    (string-listp nms))
  :rule-classes :rewrite)