• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
          • Sothm-inst-facts
          • Ext-fun-subst-term/terms/function
          • Fun-subst-function
          • Sothm-inst-pairs
          • Funvars-of-term/terms
          • Funvars-of-plain-fn
          • Sothm-inst-proof
          • Fun-subst-term/terms
          • Get-sof-instance
          • Sof-instancesp
          • Put-sof-instance
          • Fun-substp
          • Sofun-kindp
          • Funvar-listp
          • *-listp
          • Funvars-of-quantifier-fn
          • No-trivial-pairsp
          • Funvars-of-choice-fn
          • Funvar-instp
          • Funvars-of-thm
          • Sofunp
          • Funvarp
          • Sof-instances
          • Sothmp
          • Quant-sofunp
          • Plain-sofunp
          • Funvar-inst-listp
          • Choice-sofunp
          • Sofun-funvars
          • Sofun-kind
          • Function-variables-table
          • Sof-instances-table
          • Second-order-functions-table
        • Gen-macro2-of-macro
        • Defun-inst-implementation
        • 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

• Soft-implementation-core

Sof-instances

Known instances of a second-order function.

Signature

(sof-instances sofun wrld) → instmap

Arguments

sofun — Guard (sofunp sofun wrld).

wrld — Guard (plist-worldp wrld).

Returns

instmap — A sof-instancesp.

Definitions and Theorems

Function: sof-instances

(defun sof-instances (sofun wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (sofunp sofun wrld))))
  (let ((__function__ 'sof-instances))
    (declare (ignorable __function__))
    (let ((table (table-alist 'sof-instances wrld)
))
      (cdr (assoc-eq sofun table)))))