		Search-engine friendly clone of the ACL2 documentation.

Create-arg-doc

Signature
(create-arg-doc x) → xstr
Arguments: x — Guard (operand-type-p x).
Returns: xstr — Type (stringp xstr).

Definitions and Theorems

Function: create-arg-doc

(defun create-arg-doc (x)
 (declare (xargs :guard (operand-type-p x)))
 (let ((__function__ 'create-arg-doc))
  (declare (ignorable __function__))
  (cond
   ((atom x) " ")
   ((eql (len x) 1)
    (b*
      ((possible-code (nth 0 x))
       (codestr (str::pretty possible-code
                             :config *x86isa-printconfig-base-10*))
       (topic-name (str::cat codestr "-Z-ADDRESSING-METHOD")))
      (if (addressing-method-code-p possible-code)
          (str::cat "[<a href=\"index.html?topic=X86ISA____"
                    topic-name "\">" codestr "</a>] ")
        (str::cat "[@('" codestr "')] "))))
   ((eql (len x) 2)
    (b*
     ((addressing-mode (nth 0 x))
      (addressing-mode-str
           (str::pretty addressing-mode
                        :config *x86isa-printconfig-base-10*))
      (addressing-mode-topic-name (str::cat addressing-mode-str
                                            "-Z-ADDRESSING-METHOD"))
      (operand-code (nth 1 x))
      (operand-code-str
       (str::pretty operand-code
                    :config *x86isa-printconfig-base-10-lowercase*))
      (operand-code-topic-name
           (str::upcase-string (str::cat operand-code-str
                                         "-OPERAND-TYPE-CODE"))))
     (str::cat "[<a href=\"index.html?topic=X86ISA____"
               addressing-mode-topic-name
               "\">" addressing-mode-str
               "</a> - <a href=\"index.html?topic=X86ISA____"
               operand-code-topic-name
               "\">" operand-code-str "</a>] ")))
   (t " "))))

Theorem: stringp-of-create-arg-doc

(defthm stringp-of-create-arg-doc
  (b* ((xstr (create-arg-doc x)))
    (stringp xstr))
  :rule-classes :rewrite)