		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-do-merges

Combine the occurrences in the merge alist into single occurrences.

Signature
(vl-lucid-do-merges merge) → merged
Arguments: merge — Guard (vl-lucidmergealist-p merge).
Returns: merged — Type (vl-lucidocclist-p merged).

Definitions and Theorems

Function: vl-lucid-do-merges

(defun vl-lucid-do-merges (merge)
  (declare (xargs :guard (vl-lucidmergealist-p merge)))
  (let ((__function__ 'vl-lucid-do-merges))
    (declare (ignorable __function__))
    (b* ((merge (vl-lucidmergealist-fix merge))
         ((when (atom merge)) nil)
         ((cons ?ctx1 occs1) (first merge)))
      (append (vl-lucid-do-merges1 occs1)
              (vl-lucid-do-merges (rest merge))))))

Theorem: vl-lucidocclist-p-of-vl-lucid-do-merges

(defthm vl-lucidocclist-p-of-vl-lucid-do-merges
  (b* ((merged (vl-lucid-do-merges merge)))
    (vl-lucidocclist-p merged))
  :rule-classes :rewrite)

Theorem: vl-lucid-do-merges-of-vl-lucidmergealist-fix-merge

(defthm vl-lucid-do-merges-of-vl-lucidmergealist-fix-merge
  (equal (vl-lucid-do-merges (vl-lucidmergealist-fix merge))
         (vl-lucid-do-merges merge)))

Theorem: vl-lucid-do-merges-vl-lucidmergealist-equiv-congruence-on-merge

(defthm
    vl-lucid-do-merges-vl-lucidmergealist-equiv-congruence-on-merge
  (implies (vl-lucidmergealist-equiv merge merge-equiv)
           (equal (vl-lucid-do-merges merge)
                  (vl-lucid-do-merges merge-equiv)))
  :rule-classes :congruence)