		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-table-lookup

Retrieve information about a shallowly embedded C structure.

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

Definitions and Theorems

Function: defstruct-table-lookup

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

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

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