		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-repetition-table-macro

Generate the defparse-name-repetition-table described in the defdefparse user documentation.

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

Definitions and Theorems

Function: defdefparse-gen-repetition-table-macro

(defun defdefparse-gen-repetition-table-macro
       (name pkg-wit table-name prefix)
 (declare (xargs :guard (and (common-lisp::symbolp name)
                             (common-lisp::symbolp pkg-wit)
                             (common-lisp::symbolp table-name)
                             (common-lisp::symbolp prefix))))
 (let ((__function__ 'defdefparse-gen-repetition-table-macro))
  (declare (ignorable __function__))
  (b* ((macro-name (packn-pos (list 'defparse-
                                    name '-repetition-table)
                              pkg-wit)))
   (cons
    'defmacro
    (cons
     macro-name
     (cons
      '(&rest args)
      (cons
       (cons
        'cons
        (cons
         ''make-event
         (cons
          (cons
           'cons
           (cons
            (cons
             'cons
             (cons
              ''defdefparse-gen-repetition-table
              (cons
               (cons
                'cons
                (cons
                 '(cons 'quote (cons args 'nil))
                 (cons
                  (cons
                   'cons
                   (cons
                    (cons
                     'cons
                     (cons
                      ''quote
                      (cons
                        (cons 'cons
                              (cons (cons 'quote (cons prefix 'nil))
                                    '('nil)))
                        'nil)))
                    (cons
                     (cons
                      'cons
                      (cons
                       (cons
                        'cons
                        (cons
                         ''quote
                         (cons
                          (cons
                           'cons
                           (cons
                                (cons 'quote (cons table-name 'nil))
                                '('nil)))
                          'nil)))
                       '('nil)))
                     'nil)))
                  'nil)))
               'nil)))
            '('nil)))
          'nil)))
       'nil)))))))

Theorem: pseudo-event-formp-of-defdefparse-gen-repetition-table-macro

(defthm pseudo-event-formp-of-defdefparse-gen-repetition-table-macro
  (b* ((event (defdefparse-gen-repetition-table-macro
                   name pkg-wit table-name prefix)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)