(vl-line-up-define-formals-and-actuals formals actuals name loc) → (mv successp subst)
Function:
(defun vl-line-up-define-formals-and-actuals (formals actuals name loc) (declare (xargs :guard (and (vl-define-formallist-p formals) (string-listp actuals) (stringp name) (vl-location-p loc)))) (let ((__function__ 'vl-line-up-define-formals-and-actuals)) (declare (ignorable __function__)) (b* (((when (atom formals)) (if (atom actuals) (mv t nil) (mv (cw "Preprocessor error (~s0): too many arguments given to ~s1." (vl-location-string loc) name) nil))) ((when (atom actuals)) (if (vl-check-remaining-formals-all-have-defaults formals name loc) (mv t (pairlis$ (vl-define-formallist->names formals) (vl-define-formallist->defaults formals))) (mv nil nil))) ((mv okp rest-subst) (vl-line-up-define-formals-and-actuals (cdr formals) (cdr actuals) name loc)) ((unless okp) (mv nil nil)) ((vl-define-formal formal1) (car formals)) (actual1 (str::trim (car actuals))) (value1 (if (equal actual1 "") (str::trim formal1.default) actual1))) (mv t (cons (cons formal1.name value1) rest-subst)))))
Theorem:
(defthm booleanp-of-vl-line-up-define-formals-and-actuals.successp (b* (((mv ?successp common-lisp::?subst) (vl-line-up-define-formals-and-actuals formals actuals name loc))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-line-up-define-formals-and-actuals.subst (b* (((mv ?successp common-lisp::?subst) (vl-line-up-define-formals-and-actuals formals actuals name loc))) (and (alistp subst) (string-listp (alist-keys subst)) (string-listp (alist-vals subst)))) :rule-classes :rewrite)