Map c$::expr-list over a list.
(expr-ident-list idents) → exprs
Function:
(defun expr-ident-list (idents) (declare (xargs :guard (ident-listp idents))) (let ((__function__ 'expr-ident-list)) (declare (ignorable __function__)) (if (endp idents) nil (cons (expr-ident (first idents)) (expr-ident-list (rest idents))))))
Theorem:
(defthm expr-listp-of-expr-ident-list (b* ((exprs (expr-ident-list idents))) (expr-listp exprs)) :rule-classes :rewrite)