		Search-engine friendly clone of the ACL2 documentation.

Defobject-implementation

Defobject-process-inputs

Process the inputs of defobject.

Signature
(defobject-process-inputs name type init call wrld) → (mv erp name-string name-ident type initer? redundantp)
Arguments: call — Guard (pseudo-event-formp call).; wrld — Guard (plist-worldp wrld).
Returns: name-string — A stringp.; name-ident — An identp.; type — A typep.; initer? — An initer-optionp.; redundantp — A booleanp.

Definitions and Theorems

Function: defobject-process-inputs

(defun defobject-process-inputs (name type init call wrld)
  (declare (xargs :guard (and (pseudo-event-formp call)
                              (plist-worldp wrld))))
  (let ((__function__ 'defobject-process-inputs))
    (declare (ignorable __function__))
    (b* (((reterr)
          "" (irr-ident)
          (irr-type)
          nil nil)
         ((erp name-string name-ident redundantp)
          (defobject-process-name name call wrld))
         ((when redundantp)
          (retok name-string name-ident (irr-type)
                 nil t))
         ((erp type)
          (defobject-process-type type))
         ((erp initer?)
          (defobject-process-init init type wrld)))
      (retok name-string
             name-ident type initer? nil))))