		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Funvars-of-quantifier-fn

Function variables depended on by a quantifier second-order function or by an instance of it.

Signature
(funvars-of-quantifier-fn fun wrld) → funvars
Arguments: fun — Guard (symbolp fun).; wrld — Guard (plist-worldp wrld).
Returns: funvars — A funvar-listp.

Quantifier second-order functions and their instances may depend on function variables via their matrices and via their guards (which are introduced via declare forms).

The returned list may contain duplicates.

Definitions and Theorems

Function: funvars-of-quantifier-fn

(defun funvars-of-quantifier-fn (fun wrld)
  (declare (xargs :guard (and (symbolp fun)
                              (plist-worldp wrld))))
  (let ((__function__ 'funvars-of-quantifier-fn))
    (declare (ignorable __function__))
    (let* ((matrix (defun-sk-matrix fun wrld))
           (guard (uguard fun wrld))
           (matrix-funvars (funvars-of-term matrix wrld))
           (guard-funvars (funvars-of-term guard wrld)))
      (append matrix-funvars guard-funvars))))