		Search-engine friendly clone of the ACL2 documentation.

Static-identifier-checking

Check-identifier-list

Check if all the identifiers in a list are well-formed.

Signature
(check-identifier-list idens) → _
Arguments: idens — Guard (identifier-listp idens).
Returns: _ — Type (reserr-optionp _).

Definitions and Theorems

Function: check-identifier-list

(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: reserr-optionp-of-check-identifier-list

(defthm reserr-optionp-of-check-identifier-list
  (b* ((_ (check-identifier-list idens)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: check-identifier-list-of-identifier-list-fix-idens

(defthm check-identifier-list-of-identifier-list-fix-idens
  (equal (check-identifier-list (identifier-list-fix idens))
         (check-identifier-list idens)))

Theorem: check-identifier-list-identifier-list-equiv-congruence-on-idens

(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)