Map a list of initializers with optional designations to a list of initializer expressions in the language definition.
(ldm-desiniter-list desiniters) → (mv erp exprs)
Function:
(defun ldm-desiniter-list (desiniters) (declare (xargs :guard (desiniter-listp desiniters))) (declare (xargs :guard (desiniter-list-unambp desiniters))) (let ((__function__ 'ldm-desiniter-list)) (declare (ignorable __function__)) (b* (((reterr) nil) ((when (endp desiniters)) (retok nil)) ((erp expr1) (ldm-desiniter (car desiniters))) ((erp exprs1) (ldm-desiniter-list (cdr desiniters)))) (retok (cons expr1 exprs1)))))
Theorem:
(defthm expr-listp-of-ldm-desiniter-list.exprs (b* (((mv acl2::?erp ?exprs) (ldm-desiniter-list desiniters))) (c::expr-listp exprs)) :rule-classes :rewrite)
Theorem:
(defthm ldm-desiniter-list-of-desiniter-list-fix-desiniters (equal (ldm-desiniter-list (desiniter-list-fix desiniters)) (ldm-desiniter-list desiniters)))
Theorem:
(defthm ldm-desiniter-list-desiniter-list-equiv-congruence-on-desiniters (implies (desiniter-list-equiv desiniters desiniters-equiv) (equal (ldm-desiniter-list desiniters) (ldm-desiniter-list desiniters-equiv))) :rule-classes :congruence)