		Search-engine friendly clone of the ACL2 documentation.

Create-extra-info-doc-string

Signature
(create-extra-info-doc-string info text) → doc
Arguments: text — Guard (stringp text).
Returns: doc — Type (stringp doc), given the guard.

Definitions and Theorems

Function: create-extra-info-doc-string

(defun create-extra-info-doc-string (info text)
 (declare (xargs :guard (stringp text)))
 (let ((__function__ 'create-extra-info-doc-string))
  (declare (ignorable __function__))
  (if info
   (let*
    ((info-string
      (cond
           ((symbolp info)
            (str::cat ":" (symbol-name info)))
           ((symbol-listp info)
            (symbol-list-to-string info))
           (t (str::pretty info
                           :config *x86isa-printconfig-base-10*)))))
    (str::cat "<tr><td> @('"
              text "') </td>" "<td> @('"
              info-string "') </td> </tr>"))
   "")))

Theorem: stringp-of-create-extra-info-doc-string

(defthm stringp-of-create-extra-info-doc-string
  (implies (and (stringp text))
           (b* ((doc (create-extra-info-doc-string info text)))
             (stringp doc)))
  :rule-classes :rewrite)