		Search-engine friendly clone of the ACL2 documentation.

Deftutorial-implementation

Deftutorial-gen-section

Generate the macro to define a section in a tutorial page.

Signature
(deftutorial-gen-section tut-name) → event
Arguments: tut-name — Guard (symbolp tut-name).
Returns: event — Type (pseudo-event-formp event).

We use a level-5 heading to keep it relatively small.

Definitions and Theorems

Function: deftutorial-gen-section

(defun deftutorial-gen-section (tut-name)
  (declare (xargs :guard (symbolp tut-name)))
  (let ((__function__ 'deftutorial-gen-section))
    (declare (ignorable __function__))
    (b* ((tut-section (add-suffix tut-name "-SECTION")))
      (cons 'defmacro
            (cons tut-section
                  '((title)
                    (cons 'xdoc::h5 (cons title 'nil))))))))

Theorem: pseudo-event-formp-of-deftutorial-gen-section

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