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