		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Get-sof-instance

Retrieve the instance associated to a given instantiation, in the map of known instances of a second-order function.

Signature
(get-sof-instance inst instmap wrld) → instance
Arguments: inst — Guard (funvar-instp inst wrld).; instmap — Guard (sof-instancesp instmap wrld).; wrld — Guard (plist-worldp wrld).
Returns: instance — Type (symbolp instance), given (sof-instancesp instmap wrld).

Instantiations are treated as equivalent according to alist-equiv. If no instance for the instantiation is found, nil is returned.

Definitions and Theorems

Function: get-sof-instance

(defun get-sof-instance (inst instmap wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (funvar-instp inst wrld)
                              (sof-instancesp instmap wrld))))
  (let ((__function__ 'get-sof-instance))
    (declare (ignorable __function__))
    (if (endp instmap)
        nil
      (let ((pair (car instmap)))
        (if (alist-equiv (car pair) inst)
            (cdr pair)
          (get-sof-instance inst (cdr instmap)
                            wrld))))))

Theorem: symbolp-of-get-sof-instance

(defthm symbolp-of-get-sof-instance
  (implies (sof-instancesp instmap wrld)
           (b* ((instance (get-sof-instance inst instmap wrld)))
             (symbolp instance)))
  :rule-classes :rewrite)