Map a list of enumerators to a list of identifiers in the language definition.
(ldm-enumer-list enumers) → (mv erp idents)
Function:
(defun ldm-enumer-list (enumers) (declare (xargs :guard (enumer-listp enumers))) (let ((__function__ 'ldm-enumer-list)) (declare (ignorable __function__)) (b* (((reterr) nil) ((when (endp enumers)) (retok nil)) ((erp ident) (ldm-enumer (car enumers))) ((erp idents) (ldm-enumer-list (cdr enumers)))) (retok (cons ident idents)))))
Theorem:
(defthm ident-listp-of-ldm-enumer-list.idents (b* (((mv acl2::?erp ?idents) (ldm-enumer-list enumers))) (c::ident-listp idents)) :rule-classes :rewrite)
Theorem:
(defthm ldm-enumer-list-of-enumer-list-fix-enumers (equal (ldm-enumer-list (enumer-list-fix enumers)) (ldm-enumer-list enumers)))
Theorem:
(defthm ldm-enumer-list-enumer-list-equiv-congruence-on-enumers (implies (enumer-list-equiv enumers enumers-equiv) (equal (ldm-enumer-list enumers) (ldm-enumer-list enumers-equiv))) :rule-classes :congruence)