		Search-engine friendly clone of the ACL2 documentation.

Create-insts-doc-aux

Signature
(create-insts-doc-aux 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-aux-fn

(defun create-insts-doc-aux-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-aux))
    (declare (ignorable __function__))
    (if (endp inst-lst)
        ""
      (concatenate 'string
                   (create-inst-doc (car inst-lst)
                                    :fn-ok? fn-ok?
                                    :arg-ok? arg-ok?)
                   (create-insts-doc-aux (cdr inst-lst)
                                         :fn-ok? fn-ok?
                                         :arg-ok? arg-ok?)))))

Theorem: stringp-of-create-insts-doc-aux

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