		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-repetition-table-name

Generate the name of the constant whose value is the table of repetition parsing functions.

Signature
(defdefparse-gen-repetition-table-name name pkg-wit) → name
Arguments: name — Guard (common-lisp::symbolp name).; pkg-wit — Guard (common-lisp::symbolp pkg-wit).
Returns: name — Type (common-lisp::symbolp name).

The constant name is in the same package as the generated macros, and includes the name passed to defdefparse.

Definitions and Theorems

Function: defdefparse-gen-repetition-table-name

(defun defdefparse-gen-repetition-table-name (name pkg-wit)
  (declare (xargs :guard (and (common-lisp::symbolp name)
                              (common-lisp::symbolp pkg-wit))))
  (let ((__function__ 'defdefparse-gen-repetition-table-name))
    (declare (ignorable __function__))
    (packn-pos (list '*defparse-
                     name '-repetition-table*)
               pkg-wit)))

Theorem: symbolp-of-defdefparse-gen-repetition-table-name

(defthm symbolp-of-defdefparse-gen-repetition-table-name
  (b* ((name (defdefparse-gen-repetition-table-name name pkg-wit)))
    (common-lisp::symbolp name))
  :rule-classes :rewrite)