mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 09:55:19 +00:00
parent
606754c09a
commit
16af728fbe
|
@ -1799,13 +1799,13 @@ namespace z3 {
|
||||||
unsigned m_index;
|
unsigned m_index;
|
||||||
public:
|
public:
|
||||||
iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
|
iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
|
||||||
iterator(iterator& other): m_vector(other.m_vector), m_index(other.m_index) {}
|
iterator(iterator const& other): m_vector(other.m_vector), m_index(other.m_index) {}
|
||||||
iterator operator=(iterator const& other) { m_vector = other.m_vector; m_index = other.m_index; return *this; }
|
iterator operator=(iterator const& other) { m_vector = other.m_vector; m_index = other.m_index; return *this; }
|
||||||
|
|
||||||
bool operator==(iterator const& other) {
|
bool operator==(iterator const& other) const {
|
||||||
return other.m_index == m_index;
|
return other.m_index == m_index;
|
||||||
};
|
};
|
||||||
bool operator!=(iterator const& other) {
|
bool operator!=(iterator const& other) const {
|
||||||
return other.m_index != m_index;
|
return other.m_index != m_index;
|
||||||
};
|
};
|
||||||
iterator& operator++() {
|
iterator& operator++() {
|
||||||
|
|
Loading…
Reference in a new issue