• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
      • Soft-future-work
      • Soft-macros
      • Updates-to-workshop-material
      • Soft-implementation
        • Soft-implementation-core
        • Gen-macro2-of-macro
        • Defun-inst-implementation
          • Defun-inst-quant-events
          • Defun-inst-plain-events
          • Defun-inst-fn
          • Defun-inst-choice-events
          • Check-qrewrite-rule-funvars
          • Check-sofun-inst
          • Show-defun-inst
          • Defun-inst-macro-definition
        • Defthm-inst-implementation
        • Defsoft-implementation
        • Defunvar-implementation
        • Defund-sk2-implementation
        • Defun-sk2-implementation
        • Define-sk2-implementation
        • Defchoose2-implementation
        • Defund2-implementation
        • Defun2-implementation
        • Define2-implementation
      • Soft-notions
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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))))