		Search-engine friendly clone of the ACL2 documentation.

Create-args-doc

Signature
(create-args-doc operands) → docstr
Arguments: operands — Guard (maybe-operands-p operands).
Returns: docstr — Type (stringp docstr).

Definitions and Theorems

Function: create-args-doc

(defun create-args-doc (operands)
  (declare (xargs :guard (maybe-operands-p operands)))
  (let ((__function__ 'create-args-doc))
    (declare (ignorable __function__))
    (b* (((unless operands) "<td> </td>")
         ((operands operands))
         (op1 (create-arg-doc operands.op1))
         ((if (eql operands.op2 nil))
          (str::cat "<td> " op1 " </td>"))
         (op2 (create-arg-doc operands.op2))
         ((if (eql operands.op3 nil))
          (str::cat "<td> " op1 ", " op2 " </td>"))
         (op3 (create-arg-doc operands.op3))
         ((if (eql operands.op4 nil))
          (str::cat "<td> " op1 ", " op2 ", " op3 " </td>"))
         (op4 (create-arg-doc operands.op4)))
      (str::cat "<td> " op1
                ", " op2 ", " op3 ", " op4 " </td>"))))

Theorem: stringp-of-create-args-doc

(defthm stringp-of-create-args-doc
  (b* ((docstr (create-args-doc operands)))
    (stringp docstr))
  :rule-classes :rewrite)