		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Functions-called

Signature
(functions-called expr) → l
Returns: l — Type (string-listp l).

Definitions and Theorems

Function: functions-called

(defun functions-called (expr)
 (declare (xargs :guard t))
 (let ((__function__ 'functions-called))
   (declare (ignorable __function__))
   (if (atom expr)
       nil
     (let ((rec-fns (append (functions-called (car expr))
                            (functions-called (cdr expr)))))
       (if (and (expressionp expr)
                (equal (expression-kind expr) ':call))
           (cons (identifier->name (expression-call->function expr))
                 rec-fns)
         rec-fns)))))

Theorem: string-listp-of-functions-called

(defthm string-listp-of-functions-called
  (b* ((l (functions-called expr)))
    (string-listp l))
  :rule-classes :rewrite)