		Search-engine friendly clone of the ACL2 documentation.

Definj-implementation

Definj-lookup

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

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

This is a wrapper of defmapping-lookup that makes sure that the \alpha conversion is an injection (and also that the left inverse \beta conversion is a surjection), i.e. that it has the :beta-of-alpha theorem. It causes an error if that is not the case.

Definitions and Theorems

Function: definj-lookup

(defun definj-lookup (name wrld)
 (declare (xargs :guard (and (symbolp name)
                             (plist-worldp wrld))))
 (let ((__function__ 'definj-lookup))
  (declare (ignorable __function__))
  (b*
   ((info (defmapping-lookup name wrld))
    ((when (not info)) nil)
    ((when (not (defmapping-info->beta-of-alpha info)))
     (raise
         "The mapping ~x0 does not have the :BETA-OF-ALPHA theorem."
         name)))
   info)))