		Search-engine friendly clone of the ACL2 documentation.

Numbered-names-in-use

Add-numbered-name-in-use

Record that a numbered name is in use.

This macro generates an event form to add a numbered name to the table of numbered names in use. If the name is not a numbered name, or it is a numbered name with a wildcard, tha table is unchanged (via an empty progn).

Macro: add-numbered-name-in-use

(defmacro add-numbered-name-in-use (name)
  (cons 'make-event
        (cons (cons 'add-numbered-name-in-use-fn
                    (cons (cons 'quote (cons name 'nil))
                          '((w state))))
              'nil)))

Definitions and Theorems

Function: add-numbered-name-in-use-fn

(defun add-numbered-name-in-use-fn (name wrld)
 (declare (xargs :guard (and (symbolp name)
                             (plist-worldp wrld))))
 (let ((__function__ 'add-numbered-name-in-use-fn))
  (declare (ignorable __function__))
  (b* (((mv is-numbered-name base index)
        (check-numbered-name name wrld)))
    (if
     (and is-numbered-name (/= index 0))
     (b* ((table (table-alist 'numbered-names-in-use
                              wrld)
)
          (current-indices (cdr (assoc-eq base table)))
          (new-indices (add-to-set-eql index current-indices)))
       (cons 'table
             (cons 'numbered-names-in-use
                   (cons (cons 'quote (cons base 'nil))
                         (cons (cons 'quote (cons new-indices 'nil))
                               'nil)))))
     '(progn)))))

Theorem: pseudo-event-formp-of-add-numbered-name-in-use-fn

(defthm pseudo-event-formp-of-add-numbered-name-in-use-fn
  (b* ((event (add-numbered-name-in-use-fn name wrld)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)