		Search-engine friendly clone of the ACL2 documentation.

Obags

Delete

Remove (an occurrence of) a value from an obag.

Signature
(delete x bag) → bag1
Arguments: bag — Guard (bagp bag).
Returns: bag1 — Type (bagp bag1).

This is similar to set::delete for osets.

Definitions and Theorems

Function: delete

(defun delete (x bag)
       (declare (xargs :guard (bagp bag)))
       (let ((__function__ 'delete))
            (declare (ignorable __function__))
            (cond ((empty bag) nil)
                  ((equal x (head bag)) (tail bag))
                  (t (cons (head bag)
                           (delete x (tail bag)))))))

Theorem: bagp-of-delete

(defthm bagp-of-delete
        (b* ((bag1 (delete x bag))) (bagp bag1))
        :rule-classes :rewrite)