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