		Search-engine friendly clone of the ACL2 documentation.

Defiso-implementation

Defiso-lookup

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

Signature
(defiso-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 mapping is an isomorphism, i.e. that it has both the :beta-of-alpha and :alpha-of-beta theorems. It causes an error if that is not the case.

Definitions and Theorems

Function: defiso-lookup

(defun defiso-lookup (name wrld)
 (declare (xargs :guard (and (symbolp name)
                             (plist-worldp wrld))))
 (let ((__function__ 'defiso-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))
    ((when (not (defmapping-info->alpha-of-beta info)))
     (raise
         "The mapping ~x0 does not have the :ALPHA-OF-BETA theorem."
         name)))
   info)))