Lift deftreeops-gen-rep-info to lists of repetitions, i.e. to concatenations.
(deftreeops-gen-rep-info-list conc i check-conc-fn alt-singletonp rulename-upstring prefix) → infos
Function:
(defun deftreeops-gen-rep-info-list (conc i check-conc-fn alt-singletonp rulename-upstring prefix) (declare (xargs :guard (and (concatenationp conc) (posp i) (common-lisp::symbolp check-conc-fn) (booleanp alt-singletonp) (common-lisp::stringp rulename-upstring) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-rep-info-list)) (declare (ignorable __function__)) (b* (((when (endp conc)) nil) (info (deftreeops-gen-rep-info (car conc) i check-conc-fn alt-singletonp rulename-upstring prefix)) (more-info (deftreeops-gen-rep-info-list (cdr conc) i check-conc-fn alt-singletonp rulename-upstring prefix))) (cons info more-info))))
Theorem:
(defthm deftreeops-rep-info-listp-of-deftreeops-gen-rep-info-list (b* ((infos (deftreeops-gen-rep-info-list conc i check-conc-fn alt-singletonp rulename-upstring prefix))) (deftreeops-rep-info-listp infos)) :rule-classes :rewrite)