		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Funvar-instp

Recognize instantiations.

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

These are non-empty function substitutions whose keys are function variables and whose values are function names.

Definitions and Theorems

Function: funvar-instp

(defun funvar-instp (inst wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (let ((__function__ 'funvar-instp))
    (declare (ignorable __function__))
    (and (fun-substp inst)
         (consp inst)
         (funvar-listp (alist-keys inst) wrld)
         (function-symbol-listp (alist-vals inst)
                                wrld))))

Theorem: booleanp-of-funvar-instp

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