		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Unop-for-opcall-name

Accessor function for *unary-opcall-name-to-unop*.

Signature
(unop-for-opcall-name name) → retval
Arguments: name — Guard (stringp name).
Returns: retval — Type (unop-resultp retval).

Definitions and Theorems

Function: unop-for-opcall-name

(defun unop-for-opcall-name (name)
 (declare (xargs :guard (stringp name)))
 (let ((__function__ 'unop-for-opcall-name))
   (declare (ignorable __function__))
   (let
      ((unop? (cdr (assoc-equal name *unary-opcall-name-to-unop*))))
     (if (not (unopp unop?))
         (reserrf (list :unknown-unary-operator-name name))
       unop?))))

Theorem: unop-resultp-of-unop-for-opcall-name

(defthm unop-resultp-of-unop-for-opcall-name
  (b* ((retval (unop-for-opcall-name name)))
    (unop-resultp retval))
  :rule-classes :rewrite)