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