Check if all the identifiers in a list are well-formed.
(check-identifier-list idens) → _
Function:
(defun check-identifier-list (idens) (declare (xargs :guard (identifier-listp idens))) (let ((__function__ 'check-identifier-list)) (declare (ignorable __function__)) (b* (((when (endp idens)) nil) ((okf &) (check-identifier (car idens))) ((okf &) (check-identifier-list (cdr idens)))) nil)))
Theorem:
(defthm reserr-optionp-of-check-identifier-list (b* ((_ (check-identifier-list idens))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm check-identifier-list-of-identifier-list-fix-idens (equal (check-identifier-list (identifier-list-fix idens)) (check-identifier-list idens)))
Theorem:
(defthm check-identifier-list-identifier-list-equiv-congruence-on-idens (implies (identifier-list-equiv idens idens-equiv) (equal (check-identifier-list idens) (check-identifier-list idens-equiv))) :rule-classes :congruence)