		Search-engine friendly clone of the ACL2 documentation.

Generic-composite-constructors

Desc

Construct an XDOC tree for a description.

This consists of a paragraph that identifies the thing(s) being described followed by a quoted block of a sequence of trees that describe the thing(s).

The first argument is either a string for a single thing being described or a list of strings for a multiple things being described. In the latter case, the strings are separated by line breaks in the generated paragraph.

An alternative to generating a paragrah followed by a quoted block, is to generate an HTML description list <dl>...</dl> with the thing(s) that are being described as term(s) <dt>...</dt> and with the description trees inside <dd>...</dd>. However, the terms in a description list are rendered in bold, so it seems preferable to use a paragraph and a quoted block.

Macro: desc

(defmacro desc (thing/things &rest description)
  (cons 'desc-fn
        (cons thing/things
              (cons (cons 'list description) 'nil))))

Definitions and Theorems

Function: desc-things-to-string

(defun desc-things-to-string (things)
  (declare (xargs :guard (string-listp things)))
  (cond ((endp things) "")
        ((endp (cdr things)) (car things))
        (t (concatenate 'string
                        (car things)
                        "<br/>"
                        (desc-things-to-string (cdr things))))))

Theorem: stringp-of-desc-things-to-string

(defthm stringp-of-desc-things-to-string
  (implies (string-listp things)
           (stringp (desc-things-to-string things))))

Function: desc-fn

(defun desc-fn (thing/things description)
  (declare (xargs :guard (and (or (stringp thing/things)
                                  (string-listp thing/things))
                              (tree-listp description))))
  (let* ((things (if (stringp thing/things)
                     (list thing/things)
                   thing/things))
         (things-string (desc-things-to-string things))
         (things-tree (p things-string))
         (description-tree (blockquote-fn nil description)))
    (&& things-tree description-tree)))