		Search-engine friendly clone of the ACL2 documentation.

Symbol-name-lst

Lift symbol-name to lists

This function returns the list of symbol-names of a given list of symbols.

Function: symbol-name-lst

(defun symbol-name-lst (lst)
  (declare (xargs :guard (symbol-listp lst)))
  (cond ((endp lst) nil)
        (t (cons (symbol-name (car lst))
                 (symbol-name-lst (cdr lst))))))

Subtopics

Std/basic/symbol-name-lst: Theorems about symbol-name-lst in the Std/basic library.