		Search-engine friendly clone of the ACL2 documentation.

Defobject-implementation

Defobject-table-lookup

Retrieve information about a shallowly embedded C external object.

Signature
(defobject-table-lookup name wrld) → info?
Arguments: name — Guard (stringp name).; wrld — Guard (plist-worldp wrld).
Returns: info? — Type (defobject-info-optionp info?).

Definitions and Theorems

Function: defobject-table-lookup

(defun defobject-table-lookup (name wrld)
 (declare (xargs :guard (and (stringp name)
                             (plist-worldp wrld))))
 (let ((__function__ 'defobject-table-lookup))
   (declare (ignorable __function__))
   (b*
     ((pair (assoc-equal name
                         (table-alist+ *defobject-table* wrld)))
      ((when (not (consp pair))) nil)
      (info (cdr pair))
      ((unless (defobject-infop info))
       (raise "Internal error: malformed DEFOBJECT information ~x0."
              info)))
     info)))

Theorem: defobject-info-optionp-of-defobject-table-lookup

(defthm defobject-info-optionp-of-defobject-table-lookup
  (b* ((info? (defobject-table-lookup name wrld)))
    (defobject-info-optionp info?))
  :rule-classes :rewrite)