		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Sof-instancesp

Recognize the information about the instances that is associated to second-order function names in the sof-instances table.

Signature
(sof-instancesp instmap wrld) → yes/no
Arguments: wrld — Guard (plist-worldp wrld).
Returns: yes/no — Type (booleanp yes/no).

This is an alist from instantiations to function names. Each pair in the alist maps an instantiation to the corresponding instance.

Definitions and Theorems

Function: sof-instancesp

(defun sof-instancesp (instmap wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (let ((__function__ 'sof-instancesp))
    (declare (ignorable __function__))
    (and (alistp instmap)
         (funvar-inst-listp (alist-keys instmap)
                            wrld)
         (symbol-listp (alist-vals instmap)))))

Theorem: booleanp-of-sof-instancesp

(defthm booleanp-of-sof-instancesp
  (b* ((yes/no (sof-instancesp instmap wrld)))
    (booleanp yes/no))
  :rule-classes :rewrite)