Generate a list of C structure declarations from a list of member types.
(atc-gen-struct-declon-list meminfos) → declons
Function:
(defun atc-gen-struct-declon-list (meminfos) (declare (xargs :guard (member-type-listp meminfos))) (let ((__function__ 'atc-gen-struct-declon-list)) (declare (ignorable __function__)) (b* (((when (endp meminfos)) nil) (meminfo (car meminfos)) ((member-type meminfo) meminfo) ((mv tyspec declor) (ident+type-to-tyspec+declor meminfo.name meminfo.type)) (declon (make-struct-declon :tyspec tyspec :declor declor)) (declons (atc-gen-struct-declon-list (cdr meminfos)))) (cons declon declons))))
Theorem:
(defthm struct-declon-listp-of-atc-gen-struct-declon-list (b* ((declons (atc-gen-struct-declon-list meminfos))) (struct-declon-listp declons)) :rule-classes :rewrite)