		Search-engine friendly clone of the ACL2 documentation.

Symbol-list-to-string

Signature
(symbol-list-to-string lst) → newstr
Arguments: lst — Guard (symbol-listp lst).
Returns: newstr — Type (stringp newstr), given the guard.

Definitions and Theorems

Function: symbol-list-to-string

(defun symbol-list-to-string (lst)
  (declare (xargs :guard (symbol-listp lst)))
  (let ((__function__ 'symbol-list-to-string))
    (declare (ignorable __function__))
    (if (atom lst)
        ""
      (if (eql (len lst) 1)
          (str::cat ":" (symbol-name (car lst)))
        (str::cat ":" (symbol-name (car lst))
                  " "
                  (symbol-list-to-string (cdr lst)))))))

Theorem: stringp-of-symbol-list-to-string

(defthm stringp-of-symbol-list-to-string
  (implies (and (symbol-listp lst))
           (b* ((newstr (symbol-list-to-string lst)))
             (stringp newstr)))
  :rule-classes :rewrite)