		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Funvarp

Recognize names of function variables.

Signature
(funvarp funvar wrld) → yes/no
Arguments: wrld — Guard (plist-worldp wrld).
Returns: yes/no — Type (booleanp yes/no).

These are symbols that name declared function variables, i.e. that are in the table of function variables.

Definitions and Theorems

Function: funvarp

(defun funvarp (funvar wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (let ((__function__ 'funvarp))
    (declare (ignorable __function__))
    (let ((table (table-alist 'function-variables wrld)
))
      (and (symbolp funvar)
           (not (null (assoc-eq funvar table)))))))

Theorem: booleanp-of-funvarp

(defthm booleanp-of-funvarp
  (b* ((yes/no (funvarp funvar wrld)))
    (booleanp yes/no))
  :rule-classes :rewrite)