Turn a list of named formulas into theorem events.
(named-formulas-to-thm-events named-formulas named-hints named-rule-classes enableds locals names-to-avoid wrld) → (mv thm-events thm-names)
Repeatedly call named-formula-to-thm-event, ensuring that all the theorem names are distinct by incrementally adding the generated names to the list of names to avoid.
Function:
(defun named-formulas-to-thm-events-aux (named-formulas named-hints named-rule-classes enableds locals names-to-avoid rev-thm-events rev-thm-names wrld) (declare (xargs :guard (and (symbol-alistp named-formulas) (symbol-alistp named-hints) (symbol-alistp named-rule-classes) (or (symbol-listp enableds) (eq enableds t)) (or (symbol-listp locals) (eq locals t)) (symbol-listp names-to-avoid) (pseudo-event-form-listp rev-thm-events) (symbol-symbol-alistp rev-thm-names) (plist-worldp wrld)))) (let ((__function__ 'named-formulas-to-thm-events-aux)) (declare (ignorable __function__)) (cond ((endp named-formulas) (mv (reverse rev-thm-events) (reverse rev-thm-names))) (t (b* ((named-formula (car named-formulas)) (name (car named-formula)) (formula (cdr named-formula)) (hints (cdr (assoc-eq name named-hints))) (rule-classes (cdr (assoc-eq name named-rule-classes))) (enabled (or (eq enableds t) (member-eq name enableds))) (local (or (eq locals t) (member-eq name locals))) ((mv thm-event thm-name) (named-formula-to-thm-event name formula hints rule-classes enabled local names-to-avoid wrld)) (names-to-avoid (cons thm-name names-to-avoid)) (rev-thm-names (acons name thm-name rev-thm-names)) (rev-thm-events (cons thm-event rev-thm-events))) (named-formulas-to-thm-events-aux (cdr named-formulas) named-hints named-rule-classes enabled locals names-to-avoid rev-thm-events rev-thm-names wrld))))))
Function:
(defun named-formulas-to-thm-events (named-formulas named-hints named-rule-classes enableds locals names-to-avoid wrld) (declare (xargs :guard (and (symbol-alistp named-formulas) (symbol-truelist-alistp named-hints) (symbol-alistp named-rule-classes) (or (symbol-listp enableds) (eq enableds t)) (or (symbol-listp locals) (eq locals t)) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'named-formulas-to-thm-events)) (declare (ignorable __function__)) (named-formulas-to-thm-events-aux named-formulas named-hints named-rule-classes enableds locals names-to-avoid nil nil wrld)))