(vl-check-remaining-formals-all-have-defaults x name loc ppst) → (mv successp ppst)
Function:
(defun vl-check-remaining-formals-all-have-defaults (x name loc ppst) (declare (xargs :stobjs (ppst))) (declare (xargs :guard (and (vl-define-formallist-p x) (stringp name) (vl-location-p loc)))) (let ((__function__ 'vl-check-remaining-formals-all-have-defaults)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t ppst)) ((vl-define-formal x1) (car x)) ((unless x1.default) (let ((ppst (vl-ppst-fatal :msg "~a0: too few arguments to ~s1 (no default value ~ for ~s2)." :args (list loc name x1.name)))) (mv nil ppst)))) (vl-check-remaining-formals-all-have-defaults (cdr x) name loc ppst))))
Theorem:
(defthm booleanp-of-vl-check-remaining-formals-all-have-defaults.successp (b* (((mv ?successp ?ppst) (vl-check-remaining-formals-all-have-defaults x name loc ppst))) (booleanp successp)) :rule-classes :type-prescription)