		Search-engine friendly clone of the ACL2 documentation.

Atc-input-processing

Atc-remove-called-fns

Remove from a list of function symbols all the functions called by a term.

Signature
(atc-remove-called-fns fns term) → new-fns
Arguments: fns — Guard (symbol-listp fns).; term — Guard (pseudo-termp term).
Returns: new-fns — Type (symbol-listp new-fns), given (symbol-listp fns).

This is used by atc-process-function; see that function's documentation for details.

Definitions and Theorems

Function: atc-remove-called-fns

(defun atc-remove-called-fns (fns term)
  (declare (xargs :guard (and (symbol-listp fns)
                              (pseudo-termp term))))
  (let ((__function__ 'atc-remove-called-fns))
    (declare (ignorable __function__))
    (cond ((endp fns) nil)
          (t (if (ffnnamep (car fns) term)
                 (atc-remove-called-fns (cdr fns) term)
               (cons (car fns)
                     (atc-remove-called-fns (cdr fns)
                                            term)))))))

Theorem: symbol-listp-of-atc-remove-called-fns

(defthm symbol-listp-of-atc-remove-called-fns
  (implies (symbol-listp fns)
           (b* ((new-fns (atc-remove-called-fns fns term)))
             (symbol-listp new-fns)))
  :rule-classes :rewrite)