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