Generate-write-fn-over-xw-thms
- Signature
(generate-write-fn-over-xw-thms
xw-flds write-fn
write-fn-formals &key (output-index '-1)
(hyps 't)
(prepwork 'nil))
→
*
Definitions and Theorems
Function: generate-write-fn-over-xw-thms-fn
(defun generate-write-fn-over-xw-thms-fn
(xw-flds write-fn write-fn-formals
output-index hyps prepwork)
(declare (xargs :guard t))
(let ((__function__ 'generate-write-fn-over-xw-thms))
(declare (ignorable __function__))
(cons 'encapsulate
(cons 'nil
(append (or prepwork nil)
(generate-write-fn-over-xw-thms-aux
xw-flds write-fn
write-fn-formals output-index hyps))))))
