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