(comb-transform->name x) → name
Function:
(defun comb-transform->name (x) (declare (xargs :guard (comb-transform-p x))) (let ((__function__ 'comb-transform->name)) (declare (ignorable __function__)) (case (tag (comb-transform-fix x)) (:balance-config "Balance") (:fraig-config "Fraig") (:rewrite-config "Rewrite") (:obs-constprop-config "Observability") (:observability-config "Observability") (:constprop-config "Constprop") (:snapshot-config "Snapshot") (:prune-config "Prune") (:unreachability-config "Unreachability") (:dom-supergates-sweep-config "Observability supergate sweep") (t "Abc simplify"))))
Theorem:
(defthm stringp-of-comb-transform->name (b* ((name (comb-transform->name x))) (stringp name)) :rule-classes :type-prescription)