Extract from a list of external declarations the list of function definitions, in the same order.
(ext-declon-list->fundef-list exts) → defs
Declarations are discarded. Only function definitions are projected.
Function:
(defun ext-declon-list->fundef-list (exts) (declare (xargs :guard (ext-declon-listp exts))) (let ((__function__ 'ext-declon-list->fundef-list)) (declare (ignorable __function__)) (b* (((when (endp exts)) nil) (ext (car exts))) (ext-declon-case ext :fundef (cons (ext-declon-fundef->get ext) (ext-declon-list->fundef-list (cdr exts))) :fun-declon (ext-declon-list->fundef-list (cdr exts)) :obj-declon (ext-declon-list->fundef-list (cdr exts)) :tag-declon (ext-declon-list->fundef-list (cdr exts))))))
Theorem:
(defthm fundef-listp-of-ext-declon-list->fundef-list (b* ((defs (ext-declon-list->fundef-list exts))) (fundef-listp defs)) :rule-classes :rewrite)
Theorem:
(defthm ext-declon-list->fundef-list-of-ext-declon-list-fix-exts (equal (ext-declon-list->fundef-list (ext-declon-list-fix exts)) (ext-declon-list->fundef-list exts)))
Theorem:
(defthm ext-declon-list->fundef-list-ext-declon-list-equiv-congruence-on-exts (implies (ext-declon-list-equiv exts exts-equiv) (equal (ext-declon-list->fundef-list exts) (ext-declon-list->fundef-list exts-equiv))) :rule-classes :congruence)