Get the default
(get-default-input-wrapper-to-old-name wrld) → kwd
See set-default-input-wrapper-to-old-name.
Function:
(defun get-default-input-wrapper-to-old-name (wrld) (declare (xargs :guard (plist-worldp wrld))) (let ((__function__ 'get-default-input-wrapper-to-old-name)) (declare (ignorable __function__)) (b* ((table (table-alist+ *defaults-table-name* wrld) ) (pair (assoc-eq :wrapper-to-old-name table)) ((unless (consp pair)) (prog2$ (raise "No :WRAPPER-TO-OLD-NAME found in APT defaults table.") :irrelevant-keyword-for-unconditional-returns-theorem)) (kwd (cdr pair)) ((unless (keywordp kwd)) (prog2$ (raise "The default :WRAPPER-TO-OLD-NAME is ~x0, ~ which is not a keyword." kwd) :irrelevant-keyword-for-unconditional-returns-theorem))) kwd)))
Theorem:
(defthm keywordp-of-get-default-input-wrapper-to-old-name (b* ((kwd (get-default-input-wrapper-to-old-name wrld))) (keywordp kwd)) :rule-classes :rewrite)