Process the
(defmapping-process-thm-enable thm-enable beta-of-alpha-thm$ alpha-of-beta-thm$ guard-thms$ ctx state) → (mv erp thm-enable$ state)
If the processing is successful, we return a normalized version of this input, namely a list of keywords that specifies which theorems must be enabled, among the ones that are generated.
Function:
(defun defmapping-process-thm-enable (thm-enable beta-of-alpha-thm$ alpha-of-beta-thm$ guard-thms$ ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (booleanp beta-of-alpha-thm$) (booleanp alpha-of-beta-thm$) (booleanp guard-thms$)))) (let ((__function__ 'defmapping-process-thm-enable)) (declare (ignorable __function__)) (b* (((when (eq thm-enable :all)) (value (defmapping-thm-keywords beta-of-alpha-thm$ alpha-of-beta-thm$ guard-thms$))) ((when (eq thm-enable :all-nonguard)) (value (set-difference-eq (defmapping-thm-keywords beta-of-alpha-thm$ alpha-of-beta-thm$ guard-thms$) '(:doma-guard :domb-guard :alpha-guard :beta-guard)))) ((unless (keyword-listp thm-enable)) (er-soft+ ctx t nil "The :THM-ENABLE input, ~x0, is not ~ :ALL, :ALL-NOGUARD, or a list of keywords." thm-enable)) ((er &) (ensure-list-has-no-duplicates$ thm-enable (msg "The :THM-ENABLE list, ~x0," thm-enable) t nil)) (thms (defmapping-thm-keywords beta-of-alpha-thm$ alpha-of-beta-thm$ guard-thms$)) ((unless (subsetp-eq thm-enable thms)) (er-soft+ ctx t nil "The :THM-ENABLE input, ~x0, is not a subset of ~ the keywords ~x1 for the generated theorems." thm-enable thms))) (value thm-enable))))
Theorem:
(defthm keyword-listp-of-defmapping-process-thm-enable.thm-enable$ (b* (((mv ?erp ?thm-enable$ ?state) (defmapping-process-thm-enable thm-enable beta-of-alpha-thm$ alpha-of-beta-thm$ guard-thms$ ctx state))) (keyword-listp thm-enable$)) :rule-classes :rewrite)