		Search-engine friendly clone of the ACL2 documentation.

Defgrammar-input-processing

Defgrammar-process-name

Process the *name* input.

Signature
(defgrammar-process-name name ctx state) → (mv erp nothing state)
Arguments: ctx — Guard (ctxp ctx).

Definitions and Theorems

Function: defgrammar-process-name

(defun defgrammar-process-name (name ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (ctxp ctx)))
 (let ((__function__ 'defgrammar-process-name))
  (declare (ignorable __function__))
  (b*
   (((unless (legal-constantp name))
     (er-soft+
      ctx t nil
      "The first input must be a legal constant name, ~
                   but ~x0 is not a legal constant name."
      name))
    ((er &)
     (ensure-symbol-is-fresh-event-name$
          name
          (msg "The constant name ~x0 specified as first input"
               name)
          'acl2::const
          nil t nil)))
   (value nil))))

Theorem: defgrammar-process-name-symbol-when-not-error

(defthm defgrammar-process-name-symbol-when-not-error
  (b* (((mv acl2::?erp ?nothing acl2::?state)
        (defgrammar-process-name name ctx state)))
    (implies (not erp)
             (common-lisp::symbolp name))))