		Search-engine friendly clone of the ACL2 documentation.

Deftutorial-implementation

Deftutorial-fn

Generate all the macros to build the tutorial.

Signature
(deftutorial-fn tut-name tut-title) → event
Arguments: tut-name — Guard (symbolp tut-name).; tut-title — Guard (stringp tut-title).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: deftutorial-fn

(defun deftutorial-fn (tut-name tut-title)
 (declare (xargs :guard (and (symbolp tut-name)
                             (stringp tut-title))))
 (let ((__function__ 'deftutorial-fn))
  (declare (ignorable __function__))
  (cons
   'progn
   (append
      (deftutorial-gen-deftop tut-name)
      (append (deftutorial-gen-defpage tut-name)
              (append (deftutorial-gen-deftopics tut-name tut-title)
                      (cons (deftutorial-gen-section tut-name)
                            'nil)))))))

Theorem: pseudo-event-formp-of-deftutorial-fn

(defthm pseudo-event-formp-of-deftutorial-fn
  (b* ((event (deftutorial-fn tut-name tut-title)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)