Included Books
other
(in-package "ACL2")
include-book
(include-book "install-not-normalized-event")
install-not-normalized$-fnfunction
(defun install-not-normalized$-fn (fn allp names-to-avoid state) (declare (xargs :stobjs state :mode :program)) (let* ((wrld (w state)) (fns (and allp (getpropc fn 'recursivep nil wrld)))) (cond ((cdr fns) (mv-let (events names names-to-avoid) (install-not-normalized-event-lst fns nil names-to-avoid wrld) (declare (ignore names names-to-avoid)) (cons 'progn events))) (t (mv-let (event name names-to-avoid) (install-not-normalized-event fn nil names-to-avoid wrld) (declare (ignore name names-to-avoid)) event)))))
install-not-normalized$macro
(defmacro install-not-normalized$ (fn &key allp names-to-avoid) `(make-event (install-not-normalized$-fn ',FN ,ALLP ,NAMES-TO-AVOID state)))
other
(defxdoc install-not-normalized$ :parents (std/system install-not-normalized) :short "<see topic='@(url install-not-normalized)'>Install the non-normalized definition</see> of a function, ensuring that the name of the theorem will not cause a conflict." :long "<p>This utility is an event which, when evaluated successfully, installs the event generated by @(tsee install-not-normalized-event). See @(see install-not-normalized-event).</p> <p>This is related to @(tsee install-not-normalized).</p> @(def install-not-normalized$)")