feat(util/buffer): add method erase_elem

This commit is contained in:
Leonardo de Moura 2015-01-01 15:12:31 -08:00
parent 57490a6431
commit 9be67bc0b1

View file

@ -153,6 +153,15 @@ public:
m_pos--; 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) { void insert(unsigned idx, T const & elem) {
using std::swap; using std::swap;
lean_assert(idx <= size()); lean_assert(idx <= size());