		Search-engine friendly clone of the ACL2 documentation.

Get-operand-type-code-doc

Signature
(get-operand-type-code-doc code) → str
Arguments: code — Guard (operand-type-code-p code).
Returns: str — Type (stringp str).

Definitions and Theorems

Function: get-operand-type-code-doc

(defun get-operand-type-code-doc (code)
  (declare (xargs :guard (operand-type-code-p code)))
  (let ((__function__ 'get-operand-type-code-doc))
    (declare (ignorable __function__))
    (b* ((alst (cdr (assoc-equal code *operand-type-code-info*)))
         (doc (cdr (assoc-equal :doc alst)))
         ((unless doc) ""))
      doc)))

Theorem: stringp-of-get-operand-type-code-doc

(defthm stringp-of-get-operand-type-code-doc
  (b* ((str (get-operand-type-code-doc code)))
    (stringp str))
  :rule-classes :rewrite)