Check if each element of a list is a symbol or not, returning a list of booleans, one per element.
(atc-symbolp-list list) → bools
This lifts symbolp to lists. Note that it differs from symbol-listp. This belongs to a more general library.
Function:
(defun atc-symbolp-list (list) (declare (xargs :guard (true-listp list))) (let ((__function__ 'atc-symbolp-list)) (declare (ignorable __function__)) (cond ((endp list) nil) (t (cons (symbolp (car list)) (atc-symbolp-list (cdr list)))))))
Theorem:
(defthm boolean-listp-of-atc-symbolp-list (b* ((bools (atc-symbolp-list list))) (boolean-listp bools)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atc-symbolp-list (b* ((?bools (atc-symbolp-list list))) (equal (len bools) (len list))))