		Search-engine friendly clone of the ACL2 documentation.

Create-insts-doc

Signature
(create-insts-doc inst-lst &key (fn-ok? 't) (arg-ok? 'nil)) → insts-doc-string
Arguments: inst-lst — Guard (inst-list-p inst-lst).; fn-ok? — Include information about the semantic function in the documentation or not.
Guard (booleanp fn-ok?).; arg-ok? — Include information about the operands (inst.operands field) in the documentation or not.
Guard (booleanp arg-ok?).
Returns: insts-doc-string — Type (stringp insts-doc-string).

Definitions and Theorems

Function: create-insts-doc-fn

(defun create-insts-doc-fn (inst-lst fn-ok? arg-ok?)
 (declare (xargs :guard (and (inst-list-p inst-lst)
                             (booleanp fn-ok?)
                             (booleanp arg-ok?))))
 (let ((__function__ 'create-insts-doc))
  (declare (ignorable __function__))
  (b*
   ((insts-doc-string (create-insts-doc-aux inst-lst
                                            :fn-ok? fn-ok?
                                            :arg-ok? arg-ok?))
    (table-header-1 "<th> Opcode </th>")
    (table-header-2 "<th> Mnemonic </th>")
    (table-header-3 "<th> Other Information </th>")
    (table-header-4 (if fn-ok? "<th> Semantic Function </th>"
                      ""))
    (table-header-5 (if arg-ok? "<th> Operands </th>" ""))
    (table-header (concatenate 'string
                               "<tr> " table-header-1 table-header-2
                               table-header-3 table-header-4
                               table-header-5 " </tr>")))
   (concatenate 'string
                "<table> " table-header
                insts-doc-string " </table>"))))

Theorem: stringp-of-create-insts-doc

(defthm stringp-of-create-insts-doc
 (b*
  ((insts-doc-string (create-insts-doc-fn inst-lst fn-ok? arg-ok?)))
  (stringp insts-doc-string))
 :rule-classes :rewrite)