		Search-engine friendly clone of the ACL2 documentation.

Defobject-implementation

Defobject-process-init-terms

Process the list :init.

Signature
(defobject-process-init-terms terms required-type wrld) → (mv erp exprs)
Arguments: terms — Guard (true-listp terms).; required-type — Guard (typep required-type).; wrld — Guard (plist-worldp wrld).
Returns: exprs — An expr-listp.

We process each item, returning the corresponding list of expressions if successful.

Definitions and Theorems

Function: defobject-process-init-terms

(defun defobject-process-init-terms (terms required-type wrld)
  (declare (xargs :guard (and (true-listp terms)
                              (typep required-type)
                              (plist-worldp wrld))))
  (let ((__function__ 'defobject-process-init-terms))
    (declare (ignorable __function__))
    (b* (((reterr) nil)
         ((when (endp terms)) (retok nil))
         ((erp expr)
          (defobject-process-init-term (car terms)
                                       required-type wrld))
         ((erp exprs)
          (defobject-process-init-terms (cdr terms)
                                        required-type wrld)))
      (retok (cons expr exprs)))))