		Search-engine friendly clone of the ACL2 documentation.

Install-not-normalized-event-lst

Create a list of event forms to install the non-normalized definitions of a list of functions, ensuring that the names of the theorems will not cause a conflict.

Signature
(install-not-normalized-event-lst fns local names-to-avoid wrld) → (mv events names updated-names-to-avoid)
Arguments: fns — Functions to install the non-normalized definitions of.
Guard (symbol-listp fns).; local — Make the event forms local or not.
Guard (booleanp local).; names-to-avoid — Avoid these as theorem names.
Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: events — A list of pseudo-event-formp values.; names — A symbol-listp: the names of the theorems.; updated-names-to-avoid — A symbol-listp: the input list names-to-avoid augmented with names.

Ensure that the names of the theorems are not already in use and are not among a list of names to avoid. Start with the default names (i.e. the concatenation of the names of each function suffixed with $not-normalized) and ensure their uniqueness via fresh-logical-name-with-$s-suffix.

Definitions and Theorems

Function: install-not-normalized-event-lst

(defun
 install-not-normalized-event-lst
 (fns local names-to-avoid wrld)
 (declare (xargs :guard (and (symbol-listp fns)
                             (booleanp local)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let
  ((__function__ 'install-not-normalized-event-lst))
  (declare (ignorable __function__))
  (cond
   ((endp fns) (mv nil nil names-to-avoid))
   (t
    (mv-let
     (event name names-to-avoid)
     (install-not-normalized-event (car fns)
                                   local names-to-avoid wrld)
     (mv-let
        (rest-events rest-names names-to-avoid)
        (install-not-normalized-event-lst (cdr fns)
                                          local names-to-avoid wrld)
        (mv (cons event rest-events)
            (cons name rest-names)
            names-to-avoid)))))))