		Search-engine friendly clone of the ACL2 documentation.

Defthm-inst-implementation

Check-sothm-inst

Recognize designations of instances of second-order theorems.

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

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

Definitions and Theorems

Function: check-sothm-inst

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