Map a list of structure declarations to a list of structure declarations in the language definition.
(ldm-structdecl-list structdecls) → (mv erp structdecls1)
Function:
(defun ldm-structdecl-list (structdecls) (declare (xargs :guard (structdecl-listp structdecls))) (declare (xargs :guard (structdecl-list-unambp structdecls))) (let ((__function__ 'ldm-structdecl-list)) (declare (ignorable __function__)) (b* (((reterr) nil) ((when (endp structdecls)) (retok nil)) ((erp structdecl1) (ldm-structdecl (car structdecls))) ((erp structdecls1) (ldm-structdecl-list (cdr structdecls)))) (retok (cons structdecl1 structdecls1)))))
Theorem:
(defthm struct-declon-listp-of-ldm-structdecl-list.structdecls1 (b* (((mv acl2::?erp ?structdecls1) (ldm-structdecl-list structdecls))) (c::struct-declon-listp structdecls1)) :rule-classes :rewrite)
Theorem:
(defthm ldm-structdecl-list-of-structdecl-list-fix-structdecls (equal (ldm-structdecl-list (structdecl-list-fix structdecls)) (ldm-structdecl-list structdecls)))
Theorem:
(defthm ldm-structdecl-list-structdecl-list-equiv-congruence-on-structdecls (implies (structdecl-list-equiv structdecls structdecls-equiv) (equal (ldm-structdecl-list structdecls) (ldm-structdecl-list structdecls-equiv))) :rule-classes :congruence)