		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-check-remaining-formals-all-have-defaults

Signature
(vl-check-remaining-formals-all-have-defaults x name loc ppst) → (mv successp ppst)
Arguments: x — Guard (vl-define-formallist-p x).; name — Name of macro being expanded, context for error messages.
Guard (stringp name).; loc — Location of macro being expanded, context for error messages.
Guard (vl-location-p loc).
Returns: successp — Type (booleanp successp).

Definitions and Theorems

Function: vl-check-remaining-formals-all-have-defaults

(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: booleanp-of-vl-check-remaining-formals-all-have-defaults.successp

(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)