		Search-engine friendly clone of the ACL2 documentation.

Defmapping-table

Defmapping-lookup

Return the information for the defmapping specified by name, or nil if there is no defmapping with that name.

Signature
(defmapping-lookup name wrld) → info?
Arguments: name — Guard (symbolp name).; wrld — Guard (plist-worldp wrld).
Returns: info? — A maybe-defmapping-infop.

Definitions and Theorems

Function: defmapping-lookup

(defun defmapping-lookup (name wrld)
 (declare (xargs :guard (and (symbolp name)
                             (plist-worldp wrld))))
 (let ((__function__ 'defmapping-lookup))
  (declare (ignorable __function__))
  (b* ((defmapping-table (table-alist *defmapping-table-name* wrld))
       (pair? (assoc-eq name defmapping-table))
       ((when (null pair?)) nil)
       (info (cdr pair?)))
    info)))