		Search-engine friendly clone of the ACL2 documentation.

Symbol-listp

Recognizer for a true list of symbols

The predicate symbol-listp tests whether its argument is a true list of symbols.

Function: symbol-listp

(defun symbol-listp (lst)
  (declare (xargs :guard t))
  (cond ((atom lst) (eq lst nil))
        (t (and (symbolp (car lst))
                (symbol-listp (cdr lst))))))

Subtopics

Std/typed-lists/symbol-listp: Lemmas about symbol-listp available in the std/typed-lists library.
Intern-list: Generate a list of symbols in some package.
Symbol-list-names: Extract the name of every symbol in a list.
Symbol-listp-basics: Basic theorems about symbol-listp, generated by std::deflist.