Build a description of the
The
This transformation input refers to the theorem that relates
the old function to either the new function or the wrapper function,
depending on the
Macro:
(defmacro xdoc::desc-apt-input-thm-enable (wrapper? &rest additional) (declare (xargs :guard (member-eq wrapper? '(:never :optional :always)))) (b* ((thm-name-ref (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-enable') — default @('t')" (cons (cons 'xdoc::p (cons '"Determines whether " (cons thm-name-ref '(" is enabled:")))) (cons '(xdoc::ul (xdoc::li "@('t'), to enable it.") (xdoc::li "@('nil'), to disable it.")) additional))))))