		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-input-processing

Defdefparse-process-name

Process the NAME input.

Signature
(defdefparse-process-name name ctx state) → (mv erp name state)
Arguments: ctx — Guard (ctxp ctx).
Returns: name — Type (common-lisp::symbolp name).

If successful, return the name, unchanged but with a stronger type.

For now we just check that this is a symbol. In the future we should probably also check that it and the :package inputs form a unique pair in the calls of defdefparse so far.

Definitions and Theorems

Function: defdefparse-process-name

(defun defdefparse-process-name (name ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (ctxp ctx)))
  (let ((__function__ 'defdefparse-process-name))
    (declare (ignorable __function__))
    (b* (((er &)
          (ensure-value-is-symbol$ name "The first input" t nil)))
      (value name))))

Theorem: symbolp-of-defdefparse-process-name.name

(defthm symbolp-of-defdefparse-process-name.name
  (b* (((mv acl2::?erp ?name acl2::?state)
        (defdefparse-process-name name ctx state)))
    (common-lisp::symbolp name))
  :rule-classes :rewrite)