Check if a list of function headers is statically well-formed.
(check-function-header-list headers ctxt) → err?
Function:
(defun check-function-header-list (headers ctxt) (declare (xargs :guard (and (function-header-listp headers) (contextp ctxt)))) (declare (xargs :guard (and (null (context->types ctxt)) (omap::emptyp (context->variables ctxt)) (null (context->obligation-vars ctxt)) (null (context->obligation-hyps ctxt))))) (let ((__function__ 'check-function-header-list)) (declare (ignorable __function__)) (b* (((when (endp headers)) nil) (err? (check-function-header (car headers) ctxt)) ((when err?) err?) (err? (check-function-header-list (cdr headers) ctxt)) ((when err?) err?)) nil)))
Theorem:
(defthm check-function-header-list-of-function-header-list-fix-headers (equal (check-function-header-list (function-header-list-fix headers) ctxt) (check-function-header-list headers ctxt)))
Theorem:
(defthm check-function-header-list-function-header-list-equiv-congruence-on-headers (implies (function-header-list-equiv headers headers-equiv) (equal (check-function-header-list headers ctxt) (check-function-header-list headers-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-function-header-list-of-context-fix-ctxt (equal (check-function-header-list headers (context-fix ctxt)) (check-function-header-list headers ctxt)))
Theorem:
(defthm check-function-header-list-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-function-header-list headers ctxt) (check-function-header-list headers ctxt-equiv))) :rule-classes :congruence)