		Search-engine friendly clone of the ACL2 documentation.

Get-addressing-method-doc

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

Definitions and Theorems

Function: get-addressing-method-doc

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

Theorem: stringp-of-get-addressing-method-doc

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