feat(util/sexpr/options): add is_eqp predicate for options

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-20 10:53:53 -08:00
parent 4838c055b8
commit daef2b7b24
2 changed files with 14 additions and 0 deletions

View file

@ -124,6 +124,17 @@ static void tst5() {
lean_assert(it2 == decls.end());
}
static void tst6() {
options opt, opt2;
lean_assert(is_eqp(opt, opt2));
opt = update(opt, name{"test", "foo"}, 10);
lean_assert(!is_eqp(opt, opt2));
opt2 = update(opt2, name{"test", "foo"}, 10);
lean_assert(!is_eqp(opt, opt2));
opt2 = opt;
lean_assert(is_eqp(opt, opt2));
}
int main() {
save_stack_info();
tst1();
@ -131,5 +142,6 @@ int main() {
tst3();
tst4();
tst5();
tst6();
return has_violations() ? 1 : 0;
}

View file

@ -53,6 +53,8 @@ public:
options update(char const * n, sexpr const & v) const { return update(name(n), v); }
template<typename T> options update(char const * n, T v) const { return update(n, sexpr(v)); }
friend bool is_eqp(options const & a, options const & b) { return is_eqp(a.m_value, b.m_value); }
/**
\brief Combine the options opts1 and opts2. The assignment in
opts2 overrides the ones in opts1.