Generate the macro to define a (non-top) page of the tutorial.
(deftutorial-gen-defpage tut-name) → events
The generated macro stores information about these pages into the table.
The information consists of a pair in the table,
whose key is the keyword
Function:
(defun deftutorial-gen-defpage (tut-name) (declare (xargs :guard (symbolp tut-name))) (let ((__function__ 'deftutorial-gen-defpage)) (declare (ignorable __function__)) (b* ((defpage (packn-pos (list 'def- tut-name '-page) tut-name)) (defpage-fn (add-suffix defpage "-FN")) (tut-table (add-suffix tut-name "-TABLE"))) (cons (cons 'defun (cons defpage-fn (cons '(page-name page-title page-text wrld) (cons (cons 'b* (cons (cons (cons 'pages (cons (cons 'cdr (cons (cons 'assoc-eq (cons ':pages (cons (cons 'table-alist (cons (cons 'quote (cons tut-table 'nil)) '(wrld))) 'nil))) 'nil)) 'nil)) (cons (cons 'page-name (cons (cons 'packn-pos (cons (cons 'list (cons (cons 'quote (cons tut-name 'nil)) '('- page-name))) (cons (cons 'quote (cons tut-name 'nil)) 'nil))) 'nil)) '((page (list* page-name page-title page-text)) (new-pages (cons page pages))))) (cons (cons 'cons (cons ''table (cons (cons 'cons (cons (cons 'quote (cons tut-table 'nil)) '((cons ':pages (cons (cons 'quote (cons new-pages 'nil)) 'nil))))) 'nil))) 'nil))) 'nil)))) (cons (cons 'defmacro (cons defpage (cons '(page-name page-title &rest page-text) (cons (cons 'cons (cons ''make-event (cons (cons 'cons (cons (cons 'cons (cons (cons 'quote (cons defpage-fn 'nil)) '((cons (cons 'quote (cons page-name 'nil)) (cons (cons 'quote (cons page-title 'nil)) (cons (cons 'quote (cons page-text 'nil)) '((w state)))))))) '('nil))) 'nil))) 'nil)))) 'nil)))))
Theorem:
(defthm pseudo-event-form-listp-of-deftutorial-gen-defpage (b* ((events (deftutorial-gen-defpage tut-name))) (pseudo-event-form-listp events)) :rule-classes :rewrite)