		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-option-table

Generate the table of option parsing functions.

Signature
(defdefparse-gen-option-table args prefix table-name) → event
Arguments: args — Guard (true-listp args).; prefix — Guard (common-lisp::symbolp prefix).; table-name — Guard (common-lisp::symbolp table-name).
Returns: event — Type (pseudo-event-formp event).

We generate a named constant defined with the alist produced by defdefparse-gen-option-alist.

Definitions and Theorems

Function: defdefparse-gen-option-table

(defun defdefparse-gen-option-table (args prefix table-name)
 (declare (xargs :guard (and (true-listp args)
                             (common-lisp::symbolp prefix)
                             (common-lisp::symbolp table-name))))
 (let ((__function__ 'defdefparse-gen-option-table))
  (declare (ignorable __function__))
  (b* ((alist (defdefparse-gen-option-alist args prefix)))
   (cons
    'defval
    (cons
     table-name
     (cons
      ':short
      (cons
       '"Table of option parsing functions."
       (cons
        (cons 'quote (cons alist 'nil))
        (cons
         '///
         (cons
          (cons 'assert-event
                (cons (cons 'defdefparse-alt-symbol-alistp
                            (cons table-name 'nil))
                      'nil))
          (cons
           (cons 'assert-event
                 (cons (cons 'no-duplicatesp-equal
                             (cons (cons 'strip-cars
                                         (cons table-name 'nil))
                                   'nil))
                       'nil))
           (cons
               (cons 'assert-event
                     (cons (cons 'no-duplicatesp-eq
                                 (cons (cons 'strip-cdrs
                                             (cons table-name 'nil))
                                       'nil))
                           'nil))
               'nil))))))))))))

Theorem: pseudo-event-formp-of-defdefparse-gen-option-table

(defthm pseudo-event-formp-of-defdefparse-gen-option-table
 (b* ((event (defdefparse-gen-option-table args prefix table-name)))
   (pseudo-event-formp event))
 :rule-classes :rewrite)