From 9be67bc0b16b25b85e5d143fb22876a33558c307 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 1 Jan 2015 15:12:31 -0800
Subject: [PATCH] feat(util/buffer): add method erase_elem

---
 src/util/buffer.h | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/util/buffer.h b/src/util/buffer.h
index eae5592e1c..b562e4f783 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -153,6 +153,15 @@ public:
         m_pos--;
     }
 
+    void erase_elem(T const & elem) {
+        for (unsigned i = 0; i < size(); i++) {
+            if (m_buffer[i] == elem) {
+                erase(i);
+                return;
+            }
+        }
+    }
+
     void insert(unsigned idx, T const & elem) {
         using std::swap;
         lean_assert(idx <= size());