diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt
index b39f01734..5d973fdcf 100644
--- a/src/tests/util/CMakeLists.txt
+++ b/src/tests/util/CMakeLists.txt
@@ -16,3 +16,6 @@ add_test(list ${CMAKE_CURRENT_BINARY_DIR}/list)
 add_executable(scoped_set scoped_set.cpp)
 target_link_libraries(scoped_set ${EXTRA_LIBS})
 add_test(scoped_set ${CMAKE_CURRENT_BINARY_DIR}/scoped_set)
+add_executable(options options.cpp)
+target_link_libraries(options ${EXTRA_LIBS})
+add_test(options ${CMAKE_CURRENT_BINARY_DIR}/options)
diff --git a/src/tests/util/options.cpp b/src/tests/util/options.cpp
new file mode 100644
index 000000000..a621fba8e
--- /dev/null
+++ b/src/tests/util/options.cpp
@@ -0,0 +1,24 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "options.h"
+#include "test.h"
+using namespace lean;
+
+static void tst1() {
+    options opt;
+    std::cout << opt << "\n";
+    opt = opt.update("tst", 10);
+    std::cout << opt << "\n";
+    opt = opt.update("foo", true);
+    std::cout << opt << "\n";
+}
+
+int main() {
+    continue_on_violation(true);
+    tst1();
+    return has_violations() ? 1 : 0;
+}
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 91f21e3b7..43a19f2e9 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1,4 +1,4 @@
 add_library(util trace.cpp debug.cpp name.cpp exception.cpp
   verbosity.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp
-  format.cpp safe_arith.cpp
+  format.cpp safe_arith.cpp options.cpp
   )
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 8224a6025..4cb36e418 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -176,6 +176,10 @@ bool operator==(name const & a, name const & b) {
     }
 }
 
+bool operator==(name const & a, char const * b) {
+    return a.m_ptr->m_is_string && strcmp(a.m_ptr->m_str, b) == 0;
+}
+
 int cmp(name::imp * i1, name::imp * i2) {
     static thread_local std::vector<name::imp *> limbs1;
     static thread_local std::vector<name::imp *> limbs2;
diff --git a/src/util/name.h b/src/util/name.h
index 82c7af267..ca4f6bfe1 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -33,6 +33,8 @@ public:
     name & operator=(name && other);
     friend bool operator==(name const & a, name const & b);
     friend bool operator!=(name const & a, name const & b) { return !(a == b); }
+    friend bool operator==(name const & a, char const * b);
+    friend bool operator!=(name const & a, char const * b) { return !(a == b); }
     // total order on hierarchical names.
     friend int cmp(name const & a, name const & b) { return cmp(a.m_ptr, b.m_ptr); }
     friend bool operator<(name const & a, name const & b) { return cmp(a, b) < 0; }
diff --git a/src/util/options.cpp b/src/util/options.cpp
new file mode 100644
index 000000000..114827d24
--- /dev/null
+++ b/src/util/options.cpp
@@ -0,0 +1,91 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "options.h"
+#include "sexpr_funcs.h"
+
+namespace lean {
+
+bool options::empty() const {
+    return is_nil(m_value);
+}
+
+bool options::size() const {
+    return length(m_value);
+}
+
+bool options::contains(name const & n) const {
+    return ::lean::contains(m_value, [&](sexpr const & p) { return to_name(head(p)) == n; });
+}
+
+bool options::contains(char const * n) const {
+    return ::lean::contains(m_value, [&](sexpr const & p) { return to_name(head(p)) == n; });
+}
+
+sexpr const & options::get_sexpr(name const & n, sexpr const & default_value) const {
+    sexpr const * r = find(m_value, [&](sexpr const & p) { return to_name(head(p)) == n; });
+    return r == nullptr ? default_value : *r;
+}
+
+int options::get_int(name const & n, int default_value) const {
+    sexpr const & r = get_sexpr(n);
+    return !is_nil(r) && is_int(r) ? to_int(r) : default_value;
+}
+
+bool options::get_bool(name const & n, bool default_value) const {
+    sexpr const & r = get_sexpr(n);
+    return !is_nil(r) && is_bool(r) ? to_bool(r) != 0 : default_value;
+}
+
+double options::get_double(name const & n, double default_value) const {
+    sexpr const & r = get_sexpr(n);
+    return !is_nil(r) && is_double(r) ? to_double(r) : default_value;
+}
+
+sexpr const & options::get_sexpr(char const * n, sexpr const & default_value) const {
+    sexpr const * r = find(m_value, [&](sexpr const & p) { return to_name(head(p)) == n; });
+    return r == nullptr ? default_value : *r;
+}
+
+int options::get_int(char const * n, int default_value) const {
+    sexpr const & r = get_sexpr(n);
+    return !is_nil(r) && is_int(r) ? to_int(r) : default_value;
+}
+
+bool options::get_bool(char const * n, bool default_value) const {
+    sexpr const & r = get_sexpr(n);
+    return !is_nil(r) && is_bool(r) ? to_bool(r) != 0 : default_value;
+}
+
+double options::get_double(char const * n, double default_value) const {
+    sexpr const & r = get_sexpr(n);
+    return !is_nil(r) && is_double(r) ? to_double(r) : default_value;
+}
+
+constexpr char const * left_angle_bracket  = "\u27E8";
+constexpr char const * right_angle_bracket = "\u27E9";
+constexpr char const * arrow               = "\u21a6";
+
+options options::update(name const & n, sexpr const & v) const {
+    return options(cons(cons(sexpr(n), v), m_value));
+}
+
+format pp(options const & o) {
+    // TODO
+    return format();
+}
+
+std::ostream & operator<<(std::ostream & out, options const & o) {
+    out << left_angle_bracket;
+    bool first = true;
+    foreach(o.m_value, [&](sexpr const & p) {
+            if (first) first = false; else out << ", ";
+            out << head(p) << " " << arrow << " " << tail(p);
+        });
+    out << right_angle_bracket;
+    return out;
+}
+}
diff --git a/src/util/options.h b/src/util/options.h
new file mode 100644
index 000000000..c51c2c3e8
--- /dev/null
+++ b/src/util/options.h
@@ -0,0 +1,50 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "sexpr.h"
+#include "format.h"
+#include "name.h"
+
+namespace lean {
+/** \brief Configuration options. */
+class options {
+    sexpr m_value;
+    options(sexpr const & v):m_value(v) {}
+public:
+    options() {}
+    options(options const & o):m_value(o.m_value) {}
+    options(options && o):m_value(std::move(o.m_value)) {}
+    ~options() {}
+
+    options & operator=(options const & o) { m_value = o.m_value; return *this; }
+
+    bool empty() const;
+    bool size() const;
+    bool contains(name const & n) const;
+    bool contains(char const * n) const;
+
+    bool          get_bool(name const & n, bool default_value=false) const;
+    int           get_int(name const & n, int default_value=0) const;
+    double        get_double(name const & n, double default_value=0.0) const;
+    sexpr const & get_sexpr(name const & n, sexpr const & default_value=sexpr()) const;
+
+    bool          get_bool(char const * n, bool default_value=false) const;
+    int           get_int(char const * n, int default_value=0) const;
+    double        get_double(char const * n, double default_value=0.0) const;
+    sexpr const & get_sexpr(char const * n, sexpr const & default_value=sexpr()) const;
+
+    options update(name const & n, sexpr const & v) const;
+    template<typename T> options update(name const & n, T v) const { return update(n, sexpr(v)); }
+    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 format pp(options const & o);
+    friend std::ostream & operator<<(std::ostream & out, options const & o);
+};
+template<typename T> options update(options const & o, name const & n, T const & v) { return o.update(n, sexpr(v)); }
+template<typename T> options update(options const & o, char const * n, T const & v) { return o.update(name(n), sexpr(v)); }
+}
diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp
index 75f1128eb..bbf4e9b21 100644
--- a/src/util/sexpr/sexpr.cpp
+++ b/src/util/sexpr/sexpr.cpp
@@ -43,6 +43,14 @@ struct sexpr_int : public sexpr_cell {
         m_value(v) {}
 };
 
+/** \brief S-expression cell: bool atom */
+struct sexpr_bool : public sexpr_cell {
+    bool m_value;
+    sexpr_bool(bool v):
+        sexpr_cell(sexpr_kind::BOOL, v),
+        m_value(v) {}
+};
+
 /** \brief S-expression cell: double atom */
 struct sexpr_double : public sexpr_cell {
     double m_value;
@@ -89,6 +97,7 @@ void sexpr_cell::dealloc() {
     switch (m_kind) {
     case sexpr_kind::NIL:         lean_unreachable();                      break;
     case sexpr_kind::STRING:      delete static_cast<sexpr_string*>(this); break;
+    case sexpr_kind::BOOL:        delete static_cast<sexpr_bool*>(this);   break;
     case sexpr_kind::INT:         delete static_cast<sexpr_int*>(this);    break;
     case sexpr_kind::DOUBLE:      delete static_cast<sexpr_double*>(this); break;
     case sexpr_kind::NAME:        delete static_cast<sexpr_name*>(this);   break;
@@ -100,6 +109,7 @@ void sexpr_cell::dealloc() {
 
 sexpr::sexpr(char const * v):m_ptr(new sexpr_string(v)) {}
 sexpr::sexpr(std::string const & v):m_ptr(new sexpr_string(v)) {}
+sexpr::sexpr(bool v):m_ptr(new sexpr_bool(v)) {}
 sexpr::sexpr(int v):m_ptr(new sexpr_int(v)) {}
 sexpr::sexpr(double v):m_ptr(new sexpr_double(v)) {}
 sexpr::sexpr(name const & v):m_ptr(new sexpr_name(v)) {}
@@ -122,6 +132,7 @@ sexpr_kind sexpr::kind() const { return m_ptr ? m_ptr->m_kind : sexpr_kind::NIL;
 sexpr const & head(sexpr const & s) { lean_assert(is_cons(s)); return static_cast<sexpr_cons*>(s.m_ptr)->m_head; }
 sexpr const & tail(sexpr const & s) { lean_assert(is_cons(s)); return static_cast<sexpr_cons*>(s.m_ptr)->m_tail; }
 std::string const & sexpr::get_string() const { return static_cast<sexpr_string*>(m_ptr)->m_value; }
+bool sexpr::get_bool() const { return static_cast<sexpr_bool*>(m_ptr)->m_value; }
 int sexpr::get_int() const { return static_cast<sexpr_int*>(m_ptr)->m_value; }
 double sexpr::get_double() const { return static_cast<sexpr_double*>(m_ptr)->m_value; }
 name const & sexpr::get_name() const { return static_cast<sexpr_name*>(m_ptr)->m_value; }
@@ -173,6 +184,7 @@ bool operator==(sexpr const & a, sexpr const & b) {
     switch (ka) {
     case sexpr_kind::NIL:         return true;
     case sexpr_kind::STRING:      return to_string(a) == to_string(b);
+    case sexpr_kind::BOOL:        return to_bool(a) == to_bool(b);
     case sexpr_kind::INT:         return to_int(a) == to_int(b);
     case sexpr_kind::DOUBLE:      return to_double(a) == to_double(b);
     case sexpr_kind::NAME:        return to_name(a) == to_name(b);
@@ -197,6 +209,7 @@ int cmp(sexpr const & a, sexpr const & b) {
     switch (ka) {
     case sexpr_kind::NIL:         return 0;
     case sexpr_kind::STRING:      return strcmp(to_string(a).c_str(), to_string(b).c_str());
+    case sexpr_kind::BOOL:        return to_bool(a) == to_bool(b) ? 0 : (!to_bool(a) && to_bool(b) ? -1 : 1);
     case sexpr_kind::INT:         return to_int(a) == to_int(b) ? 0 : (to_int(a) < to_int(b) ? -1 : 1);
     case sexpr_kind::DOUBLE:      return to_double(a) == to_double(b) ? 0 : (to_double(a) < to_double(b) ? -1 : 1);
     case sexpr_kind::NAME:        return cmp(to_name(a), to_name(b));
@@ -215,6 +228,7 @@ std::ostream & operator<<(std::ostream & out, sexpr const & s) {
     switch (s.kind()) {
     case sexpr_kind::NIL:         out << "nil"; break;
     case sexpr_kind::STRING:      out << "\"" << escaped(to_string(s).c_str()) << "\""; break;
+    case sexpr_kind::BOOL:        out << (to_bool(s) ? "true" : "false"); break;
     case sexpr_kind::INT:         out << to_int(s); break;
     case sexpr_kind::DOUBLE:      out << to_double(s); break;
     case sexpr_kind::NAME:        out << to_name(s); break;
diff --git a/src/util/sexpr/sexpr.h b/src/util/sexpr/sexpr.h
index cc6423744..b1e0d1471 100644
--- a/src/util/sexpr/sexpr.h
+++ b/src/util/sexpr/sexpr.h
@@ -13,7 +13,7 @@ class mpq;
 class mpz;
 struct sexpr_cell;
 
-enum class sexpr_kind { NIL, STRING, INT, DOUBLE, NAME, MPZ, MPQ, CONS };
+enum class sexpr_kind { NIL, STRING, BOOL, INT, DOUBLE, NAME, MPZ, MPQ, CONS };
 
 /**
    \brief Simple LISP-like S-expressions.
@@ -30,6 +30,7 @@ public:
     sexpr():m_ptr(nullptr) {}
     explicit sexpr(char const * v);
     explicit sexpr(std::string const & v);
+    explicit sexpr(bool v);
     explicit sexpr(int v);
     explicit sexpr(double v);
     explicit sexpr(name const & v);
@@ -60,6 +61,7 @@ public:
 
     std::string const & get_string() const;
     int get_int() const;
+    bool get_bool() const;
     double get_double() const;
     name const & get_name() const;
     mpz const & get_mpz() const;
@@ -101,6 +103,7 @@ inline bool is_atom(sexpr const & s)   { return s.kind() != sexpr_kind::CONS; }
 /** \brief Return true iff \c s is not a cons cell. */
 inline bool is_cons(sexpr const & s)   { return s.kind() == sexpr_kind::CONS; }
 inline bool is_string(sexpr const & s) { return s.kind() == sexpr_kind::STRING; }
+inline bool is_bool(sexpr const & s)   { return s.kind() == sexpr_kind::BOOL; }
 inline bool is_int(sexpr const & s)    { return s.kind() == sexpr_kind::INT; }
 inline bool is_double(sexpr const & s) { return s.kind() == sexpr_kind::DOUBLE; }
 inline bool is_name(sexpr const & s)   { return s.kind() == sexpr_kind::NAME; }
@@ -108,6 +111,7 @@ inline bool is_mpz(sexpr const & s)    { return s.kind() == sexpr_kind::MPZ; }
 inline bool is_mpq(sexpr const & s)    { return s.kind() == sexpr_kind::MPQ; }
 
 inline std::string const & to_string(sexpr const & s) { return s.get_string(); }
+inline bool to_bool(sexpr const & s) { return s.get_bool(); }
 inline int to_int(sexpr const & s) { return s.get_int(); }
 inline double to_double(sexpr const & s) { return s.get_double(); }
 inline name const & to_name(sexpr const & s) { return s.get_name(); }
@@ -128,6 +132,7 @@ inline unsigned len(sexpr const & s) { return length(s); }
     \warning This is not pointer equality.
 */
 bool operator==(sexpr const & a, sexpr const & b);
+inline bool operator==(sexpr const & a, bool b) { return is_int(a) && to_bool(a) == b; }
 inline bool operator==(sexpr const & a, int b) { return is_int(a) && to_int(a) == b; }
 inline bool operator==(sexpr const & a, double b) { return is_double(a) && to_double(a) == b; }
 inline bool operator==(sexpr const & a, std::string const & b) { return is_string(a) && to_string(a) == b; }
diff --git a/src/util/sexpr/sexpr_funcs.h b/src/util/sexpr/sexpr_funcs.h
index 080215d67..376070101 100644
--- a/src/util/sexpr/sexpr_funcs.h
+++ b/src/util/sexpr/sexpr_funcs.h
@@ -96,12 +96,14 @@ bool contains(sexpr const & l, P p) {
     static_assert(std::is_same<typename std::result_of<P(sexpr const &)>::type, bool>::value,
                   "contains: return type of p is not bool");
     lean_assert(is_list(l));
-    if (is_nil(l)) {
-        return false;
-     } else {
-        lean_assert(is_cons(l));
-        return p(head(l)) || contains(tail(l), p);
+    sexpr const * h = &l;
+    while (!is_nil(*h)) {
+        lean_assert(is_cons(*h));
+        if (p(head(*h)))
+            return true;
+        h = &tail(*h);
     }
+    return false;
 }
 
 template<typename T>
@@ -116,6 +118,21 @@ bool member(T const & e, sexpr const & l) {
     return false;
 }
 
+template<typename P>
+sexpr const * find(sexpr const & l, P p) {
+    static_assert(std::is_same<typename std::result_of<P(sexpr const &)>::type, bool>::value,
+                  "find: return type of p is not bool");
+    lean_assert(is_list(l));
+    sexpr const * h = &l;
+    while (!is_nil(*h)) {
+        lean_assert(is_cons(*h));
+        if (p(head(*h)))
+            return &(head(*h));
+        h = &tail(*h);
+    }
+    return nullptr;
+}
+
 sexpr append(sexpr const & l1, sexpr const & l2);
 
 sexpr reverse(sexpr const & l);