		Search-engine friendly clone of the ACL2 documentation.

Defun-inst-implementation

Check-sofun-inst

Recognize designations of instances of second-order functions.

Signature
(check-sofun-inst sofun-inst wrld) → yes/no
Arguments: wrld — Guard (plist-worldp wrld).
Returns: yes/no — A booleanp.

A designation of an instance of a second-order function has the form (sofun (f1 . g1) ... (fM . gM)), where sofun is a second-order function and ((f1 . g1) ... (fM . gM)) is an instantiation. These designations are used in defun-inst.

Definitions and Theorems

Function: check-sofun-inst

(defun check-sofun-inst (sofun-inst wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (let ((__function__ 'check-sofun-inst))
    (declare (ignorable __function__))
    (and (true-listp sofun-inst)
         (>= (len sofun-inst) 2)
         (sofunp (car sofun-inst) wrld)
         (funvar-instp (cdr sofun-inst) wrld))))