		Search-engine friendly clone of the ACL2 documentation.

Generic-composite-constructors

Codeblock

Construct an XDOC tree for a code block @({...}) from a sequence of strings.

The arguments must evaluate to strings that are the lines of the code block, starting with spaces appropriate for the desired indentation and with no ending new line characters. New line characters are automatically added at the end of each line. A new line character is also automatically added before all the lines, to ensure the proper formatting in the final XDOC string.

Since the XDOC tree is constructed from a sequence of subtrees, the aforementioned newlines are not directly concatenated with the input strings. Instead, each input string is turned into two strings.

This XDOC constructor provides a possibly more convenient way to enter the lines that form the code block, compared to the bare @{} XDOC constructor.

Macro: codeblock

(defmacro codeblock (&rest lines)
  (cons 'codeblock-fn
        (cons (cons 'list lines) 'nil)))

Definitions and Theorems

Function: codeblock-terminate-lines

(defun codeblock-terminate-lines (lines)
  (declare (xargs :guard (string-listp lines)))
  (cond ((endp lines) nil)
        (t (list* (car lines)
                  *newline*
                  (codeblock-terminate-lines (cdr lines))))))

Theorem: string-listp-of-codeblock-terminate-lines

(defthm string-listp-of-codeblock-terminate-lines
  (implies (string-listp lines)
           (string-listp (codeblock-terminate-lines lines))))

Function: codeblock-fn

(defun codeblock-fn (lines)
  (declare (xargs :guard (string-listp lines)))
  (@{}-fn (cons *newline*
                (codeblock-terminate-lines lines))))