Build a description of the
The
The theorem relates the old function to the new function
when there is no wrapper function,
while it relates the old function to the wrapper function
where there is a wrapper function.
Thus, the description is tailored based on the
Macro:
(defmacro xdoc::desc-apt-input-thm-name (wrapper? &rest additional) (declare (xargs :guard (member-eq wrapper? '(:never :optional :always)))) (b* ((new/wrapper-ref (case wrapper? (:never "@('new')") (:optional "@('new') (if the @(':wrapper') input is @('nil')) or @('wrapper') (if the @(':wrapper') input is @('t'))") (:always "@('wrapper')"))) (thm-name (case wrapper? (:never "@('old-to-new')") (:optional "@('old-to-new') (if the @(':wrapper') input is @('nil')) or @('old-to-wrapper') (if the @(':wrapper') input is @('t'))") (:always "@('old-to-wrapper')")))) (cons 'xdoc::desc (cons '"@('thm-name') — default @(':auto')" (cons (cons 'xdoc::p (cons '"Determines the name of the theorem that relates @('old') to " (cons new/wrapper-ref '(":")))) (cons (cons 'xdoc::ul (cons (cons 'xdoc::li (cons '"@(':auto'), to use the " (cons '(xdoc::seetopic "acl2::paired-names" "paired name") (cons '" obtained by " (cons '(xdoc::seetopic "acl2::make-paired-name" "pairing") (cons '" the name of @('old') and the name of " (cons new/wrapper-ref (cons '", putting the result into the same package as " (cons new/wrapper-ref '(".")))))))))) '((xdoc::li "Any other symbol (that is not in the main Lisp package and that is not a keyword), to use as the name of the theorem.")))) (cons (cons 'xdoc::p (cons '"In the rest of this documentation page, let " (cons thm-name '(" be this theorem.")))) additional)))))))