		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 ((emptyp 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)