Lift name-to-symbol to a mapping from sets of strings to lists of symbols.
(name-set-to-symbol-list names state) → syms
The order of the list is according to the total order that osets are based on.
Function:
(defun name-set-to-symbol-list (names state) (declare (xargs :stobjs (state))) (declare (xargs :guard (string-setp names))) (let ((__function__ 'name-set-to-symbol-list)) (declare (ignorable __function__)) (cond ((emptyp names) nil) (t (cons (name-to-symbol (head names) state) (name-set-to-symbol-list (tail names) state))))))
Theorem:
(defthm symbol-listp-of-name-set-to-symbol-list (b* ((syms (name-set-to-symbol-list names state))) (symbol-listp syms)) :rule-classes :rewrite)