		Search-engine friendly clone of the ACL2 documentation.

Defaults-table

Get-default-input-old-to-wrapper-name

Get the default :old-to-wrapper-name input of APT transformations.

Signature
(get-default-input-old-to-wrapper-name wrld) → kwd
Arguments: wrld — Guard (plist-worldp wrld).
Returns: kwd — Type (keywordp kwd).

See set-default-input-old-to-wrapper-name.

Definitions and Theorems

Function: get-default-input-old-to-wrapper-name

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

Theorem: keywordp-of-get-default-input-old-to-wrapper-name

(defthm keywordp-of-get-default-input-old-to-wrapper-name
  (b* ((kwd (get-default-input-old-to-wrapper-name wrld)))
    (keywordp kwd))
  :rule-classes :rewrite)