		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Put-sof-instance

Associates an instantiation with an instance in an existing map of know instances of a second-order function.

Signature
(put-sof-instance inst fun instmap wrld) → new-instmap
Arguments: inst — Guard (funvar-instp inst wrld).; fun — Guard (symbolp fun).; instmap — Guard (and (sof-instancesp instmap wrld) (null (get-sof-instance inst instmap wrld))) .; wrld — Guard (plist-worldp wrld).
Returns: new-instmap — A sof-instancesp.

The guard requires the absence of an instance for the same instantiation (equivalent up to alist-equiv).

Definitions and Theorems

Function: put-sof-instance

(defun put-sof-instance (inst fun instmap wrld)
 (declare
  (xargs
    :guard (and (symbolp fun)
                (plist-worldp wrld)
                (funvar-instp inst wrld)
                (and (sof-instancesp instmap wrld)
                     (null (get-sof-instance inst instmap wrld))))))
 (declare (ignore wrld))
 (let ((__function__ 'put-sof-instance))
   (declare (ignorable __function__))
   (acons inst fun instmap)))