		Search-engine friendly clone of the ACL2 documentation.

Deftutorial-implementation

Deftutorial-gen-deftop

Generate the macro to define the top page of the tutorial.

Signature
(deftutorial-gen-deftop tut-name) → events
Arguments: tut-name — Guard (symbolp tut-name).
Returns: events — Type (pseudo-event-form-listp events).

The generated macro stores information about the top page into the table. The information consists of a pair in the table, whose key is the keyword :top and whose value is a list (parents text1 text2 ...) obtained from the arguments of the macro.

Definitions and Theorems

Function: deftutorial-gen-deftop

(defun deftutorial-gen-deftop (tut-name)
 (declare (xargs :guard (symbolp tut-name)))
 (let ((__function__ 'deftutorial-gen-deftop))
  (declare (ignorable __function__))
  (b* ((deftop (packn-pos (list 'def- tut-name '-top)
                          tut-name))
       (deftop-fn (add-suffix deftop "-FN"))
       (tut-table (add-suffix tut-name "-TABLE")))
   (cons
    (cons
     'defun
     (cons
      deftop-fn
      (cons
       '(top-parents top-text)
       (cons
        (cons
         'b*
         (cons
          '((top (cons top-parents top-text)))
          (cons
           (cons
            'cons
            (cons
             ''table
             (cons
              (cons
                   'cons
                   (cons (cons 'quote (cons tut-table 'nil))
                         '((cons ':top
                                 (cons (cons 'quote (cons top 'nil))
                                       'nil)))))
              'nil)))
           'nil)))
        'nil))))
    (cons
     (cons
      'defmacro
      (cons
       deftop
       (cons
        '(top-parents &rest top-text)
        (cons
         (cons
          'cons
          (cons
           ''make-event
           (cons
            (cons
             'cons
             (cons
              (cons
               'cons
               (cons
                    (cons 'quote (cons deftop-fn 'nil))
                    '((cons (cons 'quote (cons top-parents 'nil))
                            (cons (cons 'quote (cons top-text 'nil))
                                  'nil)))))
              '('nil)))
            'nil)))
         'nil))))
     'nil)))))

Theorem: pseudo-event-form-listp-of-deftutorial-gen-deftop

(defthm pseudo-event-form-listp-of-deftutorial-gen-deftop
  (b* ((events (deftutorial-gen-deftop tut-name)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)