		Search-engine friendly clone of the ACL2 documentation.

Defsurj-implementation

Defsurj-lookup

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

Signature
(defsurj-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 a surjection (and also that the right inverse \beta conversion is an injection), i.e. that it has the :alpha-of-beta theorem. It causes an error if that is not the case.

Definitions and Theorems

Function: defsurj-lookup

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