diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 89e4f9c3d1..4d75a4f3fe 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -13,9 +13,9 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   attribute_manager.cpp unification_hint.cpp
   local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp
   fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp
-  mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp
+  mpq_macro.cpp replace_visitor_with_tc.cpp
   aux_definition.cpp inverse.cpp library_system.cpp pattern_attribute.cpp choice.cpp
   locals.cpp normalize.cpp discr_tree.cpp
   mt_task_queue.cpp st_task_queue.cpp task_helper.cpp
   messages.cpp message_buffer.cpp versioned_msg_buf.cpp message_builder.cpp module_mgr.cpp comp_val.cpp
-  documentation.cpp check.cpp)
+  documentation.cpp check.cpp arith_instance.cpp)
diff --git a/src/library/arith_instance.cpp b/src/library/arith_instance.cpp
new file mode 100644
index 0000000000..ba88c324ee
--- /dev/null
+++ b/src/library/arith_instance.cpp
@@ -0,0 +1,86 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/sstream.h"
+#include "library/util.h"
+#include "library/constants.h"
+#include "library/arith_instance.h"
+
+namespace lean {
+// TODO(Leo): pre compute arith_instance_info for nat, int and real
+
+arith_instance_info_ptr mk_arith_instance_info(expr const & type, level const & lvl) {
+    return std::make_shared<arith_instance_info>(type, lvl);
+}
+
+arith_instance::arith_instance(type_context & ctx, expr const & type, level const & level):
+    m_ctx(&ctx), m_info(mk_arith_instance_info(type, level)) {}
+
+arith_instance::arith_instance(type_context & ctx, expr const & type):
+    m_ctx(&ctx) {
+    if (optional<level> lvl = dec_level(get_level(ctx, type)))
+        m_info = mk_arith_instance_info(type, *lvl);
+    else
+        throw exception("failed to infer universe level");
+}
+
+expr arith_instance::mk_op(name const & op, name const & s, optional<expr> & r) {
+    if (r) return *r;
+    if (m_ctx) {
+        expr inst_type = mk_app(mk_constant(s, {m_info->m_level}), m_info->m_type);
+        if (auto inst = m_ctx->mk_class_instance(inst_type)) {
+            r = mk_app(mk_constant(op, {m_info->m_level}), m_info->m_type, *inst);
+            return *r;
+        }
+    }
+    throw exception(sstream() << "failed to synthesize '" << s << "'");
+}
+
+expr arith_instance::mk_structure(name const & s, optional<expr> & r) {
+    if (r) return *r;
+    if (m_ctx) {
+        expr inst_type = mk_app(mk_constant(s, {m_info->m_level}), m_info->m_type);
+        if (auto inst = m_ctx->mk_class_instance(inst_type)) {
+            r = *inst;
+            return *r;
+        }
+    }
+    throw exception(sstream() << "failed to synthesize '" << s << "'");
+}
+
+expr arith_instance::mk_bit1() {
+    if (!m_info->m_bit1)
+        m_info->m_bit1 = mk_app(mk_constant(get_bit1_name(), {m_info->m_level}), m_info->m_type, mk_has_one(), mk_has_add());
+    return *m_info->m_bit1;
+}
+
+expr arith_instance::mk_zero() { return mk_op(get_zero_name(), get_has_zero_name(), m_info->m_zero); }
+expr arith_instance::mk_one() { return mk_op(get_one_name(), get_has_one_name(), m_info->m_one); }
+expr arith_instance::mk_add() { return mk_op(get_add_name(), get_has_add_name(), m_info->m_add); }
+expr arith_instance::mk_sub() { return mk_op(get_sub_name(), get_has_sub_name(), m_info->m_sub); }
+expr arith_instance::mk_neg() { return mk_op(get_neg_name(), get_has_neg_name(), m_info->m_neg); }
+expr arith_instance::mk_mul() { return mk_op(get_mul_name(), get_has_mul_name(), m_info->m_mul); }
+expr arith_instance::mk_div() { return mk_op(get_div_name(), get_has_div_name(), m_info->m_div); }
+expr arith_instance::mk_inv() { return mk_op(get_inv_name(), get_has_inv_name(), m_info->m_inv); }
+expr arith_instance::mk_lt() { return mk_op(get_lt_name(), get_has_lt_name(), m_info->m_lt); }
+expr arith_instance::mk_le() { return mk_op(get_le_name(), get_has_le_name(), m_info->m_le); }
+
+expr arith_instance::mk_bit0() { return mk_op(get_bit0_name(), get_has_add_name(), m_info->m_bit0); }
+
+expr arith_instance::mk_weark_order() { return mk_structure(get_weak_order_name(), m_info->m_weak_order); }
+expr arith_instance::mk_add_comm_semigroup() { return mk_structure(get_add_comm_semigroup_name(), m_info->m_add_comm_semigroup); }
+expr arith_instance::mk_monoid() { return mk_structure(get_monoid_name(), m_info->m_monoid); }
+expr arith_instance::mk_add_monoid() { return mk_structure(get_add_monoid_name(), m_info->m_add_monoid); }
+expr arith_instance::mk_add_group() { return mk_structure(get_add_group_name(), m_info->m_add_group); }
+expr arith_instance::mk_add_comm_group() { return mk_structure(get_add_comm_group_name(), m_info->m_add_comm_group); }
+expr arith_instance::mk_distrib() { return mk_structure(get_distrib_name(), m_info->m_distrib); }
+expr arith_instance::mk_mul_zero_class() { return mk_structure(get_mul_zero_class_name(), m_info->m_mul_zero_class); }
+expr arith_instance::mk_semiring() { return mk_structure(get_semiring_name(), m_info->m_semiring); }
+expr arith_instance::mk_linear_ordered_semiring() { return mk_structure(get_linear_ordered_semiring_name(), m_info->m_linear_ordered_semiring); }
+expr arith_instance::mk_ring() { return mk_structure(get_ring_name(), m_info->m_ring); }
+expr arith_instance::mk_linear_ordered_ring() { return mk_structure(get_linear_ordered_ring_name(), m_info->m_linear_ordered_ring); }
+expr arith_instance::mk_field() { return mk_structure(get_field_name(), m_info->m_field); }
+}
diff --git a/src/library/arith_instance.h b/src/library/arith_instance.h
new file mode 100644
index 0000000000..95195f1055
--- /dev/null
+++ b/src/library/arith_instance.h
@@ -0,0 +1,91 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "library/type_context.h"
+
+namespace lean {
+class arith_instance_info {
+    friend class arith_instance;
+    expr  m_type;
+    level m_level;
+
+    /* Partial applications */
+    optional<expr> m_zero, m_one;
+    optional<expr> m_add, m_sub, m_neg;
+    optional<expr> m_mul, m_div, m_inv;
+    optional<expr> m_lt, m_le;
+    optional<expr> m_bit0, m_bit1;
+
+    /* Structures */
+    optional<expr> m_weak_order;
+    optional<expr> m_add_comm_semigroup;
+    optional<expr> m_monoid, m_add_monoid;
+    optional<expr> m_add_group, m_add_comm_group;
+    optional<expr> m_distrib, m_mul_zero_class;
+    optional<expr> m_semiring, m_linear_ordered_semiring;
+    optional<expr> m_ring, m_linear_ordered_ring;
+    optional<expr> m_field;
+public:
+    arith_instance_info(expr const & type, level const & lvl):m_type(type), m_level(lvl) {}
+};
+
+typedef std::shared_ptr<arith_instance_info> arith_instance_info_ptr;
+arith_instance_info_ptr mk_arith_instance_info(expr const & type, level const & lvl);
+
+class arith_instance {
+    type_context *          m_ctx;
+    arith_instance_info_ptr m_info;
+
+    expr mk_structure(name const & s, optional<expr> & r);
+    expr mk_op(name const & op, name const & s, optional<expr> & r);
+
+public:
+    arith_instance(type_context & ctx, arith_instance_info_ptr const & info):m_ctx(&ctx), m_info(info) {}
+    arith_instance(type_context & ctx, expr const & type, level const & level);
+    arith_instance(type_context & ctx, expr const & type);
+    arith_instance(arith_instance_info_ptr const & info):m_ctx(nullptr), m_info(info) {}
+
+    expr mk_zero();
+    expr mk_one();
+    expr mk_add();
+    expr mk_sub();
+    expr mk_neg();
+    expr mk_mul();
+    expr mk_div();
+    expr mk_inv();
+    expr mk_lt();
+    expr mk_le();
+
+    expr mk_bit0();
+    expr mk_bit1();
+
+    expr mk_has_zero() { return app_arg(mk_zero()); }
+    expr mk_has_one() { return app_arg(mk_one()); }
+    expr mk_has_add() { return app_arg(mk_add()); }
+    expr mk_has_sub() { return app_arg(mk_sub()); }
+    expr mk_has_neg() { return app_arg(mk_neg()); }
+    expr mk_has_mul() { return app_arg(mk_mul()); }
+    expr mk_has_div() { return app_arg(mk_div()); }
+    expr mk_has_inv() { return app_arg(mk_inv()); }
+    expr mk_has_lt() { return app_arg(mk_lt()); }
+    expr mk_has_le() { return app_arg(mk_le()); }
+
+    expr mk_weark_order();
+    expr mk_add_comm_semigroup();
+    expr mk_monoid();
+    expr mk_add_monoid();
+    expr mk_add_group();
+    expr mk_add_comm_group();
+    expr mk_distrib();
+    expr mk_mul_zero_class();
+    expr mk_semiring();
+    expr mk_linear_ordered_semiring();
+    expr mk_ring();
+    expr mk_linear_ordered_ring();
+    expr mk_field();
+};
+};
diff --git a/src/library/arith_instance_manager.cpp b/src/library/arith_instance_manager.cpp
deleted file mode 100644
index 3133f78470..0000000000
--- a/src/library/arith_instance_manager.cpp
+++ /dev/null
@@ -1,511 +0,0 @@
-/*
-  Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-  Released under Apache 2.0 license as described in the file LICENSE.
-
-  Author: Daniel Selsam
-*/
-#include "util/sstream.h"
-#include "library/constants.h"
-#include "library/app_builder.h"
-#include "library/num.h"
-#include "library/util.h"
-#include "library/cache_helper.h"
-#include "library/arith_instance_manager.h"
-
-namespace lean {
-
-static arith_instance_info_ref * g_nat_instance_info  = nullptr;
-static arith_instance_info_ref * g_int_instance_info  = nullptr;
-static arith_instance_info_ref * g_real_instance_info = nullptr;
-
-struct arith_instance_info_cache_entry {
-    local_context           m_lctx;
-    arith_instance_info_ref m_info;
-
-    arith_instance_info_cache_entry(local_context const & lctx, expr const & type, level const & l):
-        m_lctx(lctx), m_info(new arith_instance_info(type, l)) {}
-};
-
-class arith_instance_info_cache {
-private:
-    environment m_env;
-    expr_struct_map<arith_instance_info_cache_entry> m_cache;
-public:
-    environment const & env() const { return m_env; }
-    expr_struct_map<arith_instance_info_cache_entry> & get_cache() { return m_cache; }
-    arith_instance_info_cache(environment const & env): m_env(env) {}
-};
-
-typedef transparencyless_cache_compatibility_helper<arith_instance_info_cache> arith_instance_info_cache_helper;
-MK_THREAD_LOCAL_GET_DEF(arith_instance_info_cache_helper, get_aiich);
-
-static expr_struct_map<arith_instance_info_cache_entry> & get_arith_instance_info_cache_for(type_context const & tctx) {
-    return get_aiich().get_cache_for(tctx).get_cache();
-}
-
-arith_instance_info::arith_instance_info(expr const & type, level const & l):
-    m_type(type), m_level(l) {}
-
-expr arith_instance_info::get_eq() {
-    return mk_app(mk_constant(get_eq_name(), {m_level}), m_type);
-}
-
-bool arith_instance_info::is_add_group(type_context * tctx_ptr) {
-    if (m_is_add_group) {
-        return *m_is_add_group;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_add_group_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_is_add_group = optional<bool>(true);
-            return true;
-        } else {
-            m_is_add_group = optional<bool>(false);
-            return false;
-        }
-    }
-}
-
-bool arith_instance_info::is_comm_semiring(type_context * tctx_ptr) {
-    if (m_is_comm_semiring) {
-        return *m_is_comm_semiring;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_comm_semiring_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_is_comm_semiring = optional<bool>(true);
-            return true;
-        } else {
-            m_is_comm_semiring = optional<bool>(false);
-            return false;
-        }
-    }
-}
-
-bool arith_instance_info::is_comm_ring(type_context * tctx_ptr) {
-    if (m_is_comm_ring) {
-        return *m_is_comm_ring;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_comm_ring_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_is_comm_ring = optional<bool>(true);
-            return true;
-        } else {
-            m_is_comm_ring = optional<bool>(false);
-            return false;
-        }
-    }
-}
-
-bool arith_instance_info::is_linear_ordered_semiring(type_context * tctx_ptr) {
-    if (m_is_linear_ordered_semiring) {
-        return *m_is_linear_ordered_semiring;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_linear_ordered_semiring_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_is_linear_ordered_semiring = optional<bool>(true);
-            return true;
-        } else {
-            m_is_linear_ordered_semiring = optional<bool>(false);
-            return false;
-        }
-    }
-}
-
-bool arith_instance_info::is_linear_ordered_comm_ring(type_context * tctx_ptr) {
-    if (m_is_linear_ordered_comm_ring) {
-        return *m_is_linear_ordered_comm_ring;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_linear_ordered_comm_ring_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_is_linear_ordered_comm_ring = optional<bool>(true);
-            return true;
-        } else {
-            m_is_linear_ordered_comm_ring = optional<bool>(false);
-            return false;
-        }
-    }
-}
-
-bool arith_instance_info::is_field(type_context * tctx_ptr) {
-    if (m_is_field) {
-        return *m_is_field;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_field_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_is_field = optional<bool>(true);
-            return true;
-        } else {
-            m_is_field = optional<bool>(false);
-            return false;
-        }
-    }
-}
-
-bool arith_instance_info::is_discrete_field(type_context * tctx_ptr) {
-    if (m_is_discrete_field) {
-        return *m_is_discrete_field;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_discrete_field_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_is_discrete_field = optional<bool>(true);
-            return true;
-        } else {
-            m_is_discrete_field = optional<bool>(false);
-            return false;
-        }
-    }
-}
-
-optional<mpz> arith_instance_info::has_cyclic_numerals(type_context * tctx_ptr) {
-    if (!m_has_cyclic_numerals) {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_cyclic_numerals_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_has_cyclic_numerals = optional<bool>(true);
-            expr bound = tctx_ptr->whnf(mk_app(mk_constant(get_cyclic_numerals_bound_name(), {m_level}), m_type, *inst));
-            if (auto n = to_num(bound)) {
-                m_numeral_bound = *n;
-                return optional<mpz>(m_numeral_bound);
-            } else {
-                throw exception(sstream() << "bound in [cyclic_numerals " << m_type << "] must whnf to a numeral\n");
-            }
-        } else {
-            m_has_cyclic_numerals = optional<bool>(false);
-            return optional<mpz>();
-        }
-    } else if (*m_has_cyclic_numerals) {
-        return optional<mpz>(m_numeral_bound);
-    } else {
-        lean_assert(!(*m_has_cyclic_numerals));
-        return optional<mpz>();
-    }
-}
-
-expr arith_instance_info::get_zero(type_context * tctx_ptr) {
-    if (!null(m_zero)) {
-        return m_zero;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_has_zero_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_zero = mk_app(mk_constant(get_zero_name(), {m_level}), m_type, *inst);
-            return m_zero;
-        } else {
-            throw exception(sstream() << "cannot synthesize [has_zero " << m_type << "]\n");
-        }
-    }
-}
-
-expr arith_instance_info::get_one(type_context * tctx_ptr) {
-    if (!null(m_one)) {
-        return m_one;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_has_one_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_one = mk_app(mk_constant(get_one_name(), {m_level}), m_type, *inst);
-            return m_one;
-        } else {
-            throw exception(sstream() << "cannot synthesize [has_one " << m_type << "]\n");
-        }
-    }
-}
-
-expr arith_instance_info::get_bit0(type_context * tctx_ptr) {
-    if (!null(m_bit0)) {
-        return m_bit0;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_has_add_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_bit0 = mk_app(mk_constant(get_bit0_name(), {m_level}), m_type, *inst);
-            return m_bit0;
-        } else {
-            throw exception(sstream() << "cannot synthesize [has_add " << m_type << "]\n");
-        }
-    }
-}
-
-// TODO(dhs): for instances that are used for more than one getter, cache the instances in the structure as well
-expr arith_instance_info::get_bit1(type_context * tctx_ptr) {
-    if (!null(m_bit1)) {
-        return m_bit1;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type1 = mk_app(mk_constant(get_has_one_name(), {m_level}), m_type);
-        if (auto inst1 = tctx_ptr->mk_class_instance(inst_type1)) {
-            expr inst_type2 = mk_app(mk_constant(get_has_add_name(), {m_level}), m_type);
-            if (auto inst2 = tctx_ptr->mk_class_instance(inst_type2)) {
-                m_bit1 = mk_app(mk_constant(get_bit1_name(), {m_level}), m_type, *inst1, *inst2);
-                return m_bit1;
-            } else {
-                throw exception(sstream() << "cannot synthesize [has_add " << m_type << "]\n");
-            }
-        } else {
-            throw exception(sstream() << "cannot synthesize [has_one " << m_type << "]\n");
-        }
-    }
-}
-
-expr arith_instance_info::get_add(type_context * tctx_ptr) {
-    if (!null(m_add)) {
-        return m_add;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_has_add_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_add = mk_app(mk_constant(get_add_name(), {m_level}), m_type, *inst);
-            return m_add;
-        } else {
-            throw exception(sstream() << "cannot synthesize [has_add " << m_type << "]\n");
-        }
-    }
-}
-
-expr arith_instance_info::get_mul(type_context * tctx_ptr) {
-    if (!null(m_mul)) {
-        return m_mul;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_has_mul_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_mul = mk_app(mk_constant(get_mul_name(), {m_level}), m_type, *inst);
-            return m_mul;
-        } else {
-            throw exception(sstream() << "cannot synthesize [has_mul " << m_type << "]\n");
-        }
-    }
-}
-
-expr arith_instance_info::get_sub(type_context * tctx_ptr) {
-    if (!null(m_sub)) {
-        return m_sub;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_has_sub_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_sub = mk_app(mk_constant(get_sub_name(), {m_level}), m_type, *inst);
-            return m_sub;
-        } else {
-            throw exception(sstream() << "cannot synthesize [has_sub " << m_type << "]\n");
-        }
-    }
-}
-
-expr arith_instance_info::get_div(type_context * tctx_ptr) {
-    if (!null(m_div)) {
-        return m_div;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_has_div_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_div = mk_app(mk_constant(get_div_name(), {m_level}), m_type, *inst);
-            return m_div;
-        } else {
-            throw exception(sstream() << "cannot synthesize [has_div " << m_type << "]\n");
-        }
-    }
-}
-
-expr arith_instance_info::get_neg(type_context * tctx_ptr) {
-    if (!null(m_neg)) {
-        return m_neg;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_has_neg_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_neg = mk_app(mk_constant(get_neg_name(), {m_level}), m_type, *inst);
-            return m_neg;
-        } else {
-            throw exception(sstream() << "cannot synthesize [has_neg " << m_type << "]\n");
-        }
-    }
-}
-
-expr arith_instance_info::get_lt(type_context * tctx_ptr) {
-    if (!null(m_lt)) {
-        return m_lt;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_has_lt_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_lt = mk_app(mk_constant(get_lt_name(), {m_level}), m_type, *inst);
-            return m_lt;
-        } else {
-            throw exception(sstream() << "cannot synthesize [has_lt " << m_type << "]\n");
-        }
-    }
-}
-
-expr arith_instance_info::get_le(type_context * tctx_ptr) {
-    if (!null(m_le)) {
-        return m_le;
-    } else {
-        lean_assert(tctx_ptr);
-        expr inst_type = mk_app(mk_constant(get_has_le_name(), {m_level}), m_type);
-        if (auto inst = tctx_ptr->mk_class_instance(inst_type)) {
-            m_le = mk_app(mk_constant(get_le_name(), {m_level}), m_type, *inst);
-            return m_le;
-        } else {
-            throw exception(sstream() << "cannot synthesize [has_le " << m_type << "]\n");
-        }
-    }
-}
-
-// Setup and teardown
-void initialize_concrete_arith_instance_infos() {
-    // nats
-    expr nat = mk_constant(get_nat_name());
-    g_nat_instance_info = new std::shared_ptr<arith_instance_info>(new arith_instance_info(nat, mk_level_one()));
-    (*g_nat_instance_info)->m_is_field                            = optional<bool>(false);
-    (*g_nat_instance_info)->m_is_discrete_field                   = optional<bool>(false);
-    (*g_nat_instance_info)->m_is_comm_ring                        = optional<bool>(false);
-    (*g_nat_instance_info)->m_is_linear_ordered_comm_ring         = optional<bool>(false);
-    (*g_nat_instance_info)->m_is_comm_semiring                    = optional<bool>(true);
-    (*g_nat_instance_info)->m_is_linear_ordered_semiring          = optional<bool>(true);
-    (*g_nat_instance_info)->m_is_add_group                        = optional<bool>(false);
-
-    (*g_nat_instance_info)->m_has_cyclic_numerals                 = optional<bool>(false);
-
-    (*g_nat_instance_info)->m_zero    = mk_app({mk_constant(get_zero_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_zero_name())});
-    (*g_nat_instance_info)->m_one     = mk_app({mk_constant(get_one_name(), {mk_level_one()}),  nat, mk_constant(get_nat_has_one_name())});
-    (*g_nat_instance_info)->m_bit0    = mk_app({mk_constant(get_bit0_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_add_name())});
-    (*g_nat_instance_info)->m_bit1    = mk_app({mk_constant(get_bit1_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_one_name()), mk_constant(get_nat_has_add_name())});
-
-    (*g_nat_instance_info)->m_add     = mk_app({mk_constant(get_add_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_add_name())});
-    (*g_nat_instance_info)->m_mul     = mk_app({mk_constant(get_mul_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_mul_name())});
-    (*g_nat_instance_info)->m_div     = mk_app({mk_constant(get_div_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_div_name())});
-    (*g_nat_instance_info)->m_sub     = mk_app({mk_constant(get_sub_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_sub_name())});
-    (*g_nat_instance_info)->m_neg     = mk_app({mk_constant(get_neg_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_neg_name())});
-
-    (*g_nat_instance_info)->m_lt      = mk_app({mk_constant(get_lt_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_lt_name())});
-    (*g_nat_instance_info)->m_le      = mk_app({mk_constant(get_le_name(), {mk_level_one()}), nat, mk_constant(get_nat_has_le_name())});
-
-    // ints
-    expr z = mk_constant(get_int_name());
-    g_int_instance_info = new std::shared_ptr<arith_instance_info>(new arith_instance_info(z, mk_level_one()));
-    (*g_int_instance_info)->m_is_field                            = optional<bool>(false);
-    (*g_int_instance_info)->m_is_discrete_field                   = optional<bool>(false);
-    (*g_int_instance_info)->m_is_comm_ring                        = optional<bool>(true);
-    (*g_int_instance_info)->m_is_linear_ordered_comm_ring         = optional<bool>(true);
-    (*g_int_instance_info)->m_is_comm_semiring                    = optional<bool>(true);
-    (*g_int_instance_info)->m_is_linear_ordered_semiring          = optional<bool>(true);
-    (*g_int_instance_info)->m_is_add_group                        = optional<bool>(true);
-
-    (*g_int_instance_info)->m_has_cyclic_numerals                 = optional<bool>(false);
-
-    (*g_int_instance_info)->m_zero    = mk_app({mk_constant(get_zero_name(), {mk_level_one()}), z, mk_constant(get_int_has_zero_name())});
-    (*g_int_instance_info)->m_one     = mk_app({mk_constant(get_one_name(), {mk_level_one()}),  z, mk_constant(get_int_has_one_name())});
-    (*g_int_instance_info)->m_bit0    = mk_app({mk_constant(get_bit0_name(), {mk_level_one()}), z, mk_constant(get_int_has_add_name())});
-    (*g_int_instance_info)->m_bit1    = mk_app({mk_constant(get_bit1_name(), {mk_level_one()}), z, mk_constant(get_int_has_one_name()), mk_constant(get_int_has_add_name())});
-
-    (*g_int_instance_info)->m_add     = mk_app({mk_constant(get_add_name(), {mk_level_one()}), z, mk_constant(get_int_has_add_name())});
-    (*g_int_instance_info)->m_mul     = mk_app({mk_constant(get_mul_name(), {mk_level_one()}), z, mk_constant(get_int_has_mul_name())});
-    (*g_int_instance_info)->m_div     = mk_app({mk_constant(get_div_name(), {mk_level_one()}), z, mk_constant(get_int_has_div_name())});
-    (*g_int_instance_info)->m_sub     = mk_app({mk_constant(get_sub_name(), {mk_level_one()}), z, mk_constant(get_int_has_sub_name())});
-    (*g_int_instance_info)->m_neg     = mk_app({mk_constant(get_neg_name(), {mk_level_one()}), z, mk_constant(get_int_has_neg_name())});
-
-    (*g_int_instance_info)->m_lt      = mk_app({mk_constant(get_lt_name(), {mk_level_one()}), z, mk_constant(get_int_has_lt_name())});
-    (*g_int_instance_info)->m_le      = mk_app({mk_constant(get_le_name(), {mk_level_one()}), z, mk_constant(get_int_has_le_name())});
-
-    // reals
-    expr real = mk_constant(get_real_name());
-    g_real_instance_info = new std::shared_ptr<arith_instance_info>(new arith_instance_info(real, mk_level_one()));
-    (*g_real_instance_info)->m_is_field                            = optional<bool>(true);
-    (*g_real_instance_info)->m_is_discrete_field                   = optional<bool>(true);
-    (*g_real_instance_info)->m_is_comm_ring                        = optional<bool>(true);
-    (*g_real_instance_info)->m_is_linear_ordered_comm_ring         = optional<bool>(true);
-    (*g_real_instance_info)->m_is_comm_semiring                    = optional<bool>(true);
-    (*g_real_instance_info)->m_is_linear_ordered_semiring          = optional<bool>(true);
-    (*g_real_instance_info)->m_is_add_group                        = optional<bool>(true);
-
-    (*g_real_instance_info)->m_has_cyclic_numerals                 = optional<bool>(false);
-
-    (*g_real_instance_info)->m_zero    = mk_app({mk_constant(get_zero_name(), {mk_level_one()}), real, mk_constant(get_real_has_zero_name())});
-    (*g_real_instance_info)->m_one     = mk_app({mk_constant(get_one_name(), {mk_level_one()}),  real, mk_constant(get_real_has_one_name())});
-    (*g_real_instance_info)->m_bit0    = mk_app({mk_constant(get_bit0_name(), {mk_level_one()}), real, mk_constant(get_real_has_add_name())});
-    (*g_real_instance_info)->m_bit1    = mk_app({mk_constant(get_bit1_name(), {mk_level_one()}), real, mk_constant(get_real_has_one_name()), mk_constant(get_real_has_add_name())});
-
-    (*g_real_instance_info)->m_add     = mk_app({mk_constant(get_add_name(), {mk_level_one()}), real, mk_constant(get_real_has_add_name())});
-    (*g_real_instance_info)->m_mul     = mk_app({mk_constant(get_mul_name(), {mk_level_one()}), real, mk_constant(get_real_has_mul_name())});
-    (*g_real_instance_info)->m_div     = mk_app({mk_constant(get_div_name(), {mk_level_one()}), real, mk_constant(get_real_has_div_name())});
-    (*g_real_instance_info)->m_sub     = mk_app({mk_constant(get_sub_name(), {mk_level_one()}), real, mk_constant(get_real_has_sub_name())});
-    (*g_real_instance_info)->m_neg     = mk_app({mk_constant(get_neg_name(), {mk_level_one()}), real, mk_constant(get_real_has_neg_name())});
-
-    (*g_real_instance_info)->m_lt      = mk_app({mk_constant(get_lt_name(), {mk_level_one()}), real, mk_constant(get_real_has_lt_name())});
-    (*g_real_instance_info)->m_le      = mk_app({mk_constant(get_le_name(), {mk_level_one()}), real, mk_constant(get_real_has_le_name())});
-}
-
-void finalize_concrete_arith_instance_infos() {
-    delete g_real_instance_info;
-    delete g_int_instance_info;
-    delete g_nat_instance_info;
-}
-
-void initialize_arith_instance_manager() {
-    initialize_concrete_arith_instance_infos();
-}
-
-void finalize_arith_instance_manager() {
-    finalize_concrete_arith_instance_infos();
-}
-
-// Entry points
-arith_instance_info_ref get_arith_instance_info_for(concrete_arith_type type) {
-    switch (type) {
-    case concrete_arith_type::NAT:  return *g_nat_instance_info;
-    case concrete_arith_type::INT:  return *g_int_instance_info;
-    case concrete_arith_type::REAL: return *g_real_instance_info;
-    }
-    lean_unreachable();
-}
-
-optional<concrete_arith_type> is_concrete_arith_type(expr const & type) {
-    if (type == mk_constant(get_nat_name()))
-        return optional<concrete_arith_type>(concrete_arith_type::NAT);
-    if (type == mk_constant(get_int_name()))
-        return optional<concrete_arith_type>(concrete_arith_type::INT);
-    if (type == mk_constant(get_real_name()))
-        return optional<concrete_arith_type>(concrete_arith_type::REAL);
-    else
-        return optional<concrete_arith_type>();
-}
-
-arith_instance_info_ref cache_insert(expr_struct_map<arith_instance_info_cache_entry> & cache, type_context & tctx, expr const & type) {
-    auto result = cache.emplace(std::piecewise_construct,
-                                std::forward_as_tuple<expr const &>(type),
-                                // TODO(dselsam): the method initial_lctx was removed
-                                std::forward_as_tuple<local_context const &, expr const &, level const &>(tctx.lctx(), type, get_level(tctx, type)));
-//                                std::forward_as_tuple<local_context const &, expr const &, level const &>(tctx.initial_lctx(), type, get_level(tctx, type)));
-    lean_assert(result.second);
-    return result.first->second.m_info;
-}
-
-arith_instance_info_ref get_arith_instance_info_for(type_context & tctx, expr const & type) {
-    if (auto ctype = is_concrete_arith_type(type))
-        return get_arith_instance_info_for(*ctype);
-
-    expr_struct_map<arith_instance_info_cache_entry> & cache = get_arith_instance_info_cache_for(tctx);
-    auto it = cache.find(type);
-
-    if (it == cache.end()) {
-        return cache_insert(cache, tctx, type);
-    } else {
-        arith_instance_info_cache_entry & entry = it->second;
-        if (false) { // tctx.compatible_local_instances(entry.m_lctx)) { // <<< This method was removed
-            // entry.m_lctx = tctx.initial_lctx(); // << initial_lctx was removed
-            return entry.m_info;
-        } else {
-            cache.erase(type);
-            return cache_insert(cache, tctx, type);
-        }
-    }
-}
-
-}
diff --git a/src/library/arith_instance_manager.h b/src/library/arith_instance_manager.h
deleted file mode 100644
index c95d00908f..0000000000
--- a/src/library/arith_instance_manager.h
+++ /dev/null
@@ -1,75 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Daniel Selsam
-*/
-#pragma once
-#include <memory>
-#include "kernel/expr.h"
-#include "library/type_context.h"
-
-namespace lean {
-
-class arith_instance_info {
-    expr m_type;
-    level m_level;
-
-    // For boolean queries
-    optional<bool> m_is_field, m_is_discrete_field, m_is_comm_ring, m_is_linear_ordered_comm_ring;
-    optional<bool> m_is_comm_semiring, m_is_linear_ordered_semiring, m_is_add_group;
-
-    optional<bool> m_has_cyclic_numerals;
-    mpz m_numeral_bound;
-
-    // Partial applications
-    expr m_zero, m_one;
-    expr m_bit0, m_bit1;
-    expr m_add, m_mul, m_div, m_sub, m_neg;
-    expr m_eq, m_lt, m_le;
-
-    bool null(expr const & e) { return e == expr(); }
-
-    friend void initialize_concrete_arith_instance_infos();
-
-public:
-    arith_instance_info(expr const & type, level const & l);
-
-    expr get_type() const { return m_type; }
-
-    expr get_eq();
-
-    bool is_add_group(type_context * tctx_ptr = nullptr);
-    bool is_comm_semiring(type_context * tctx_ptr = nullptr);
-    bool is_comm_ring(type_context * tctx_ptr = nullptr);
-    bool is_linear_ordered_semiring(type_context * tctx_ptr = nullptr);
-    bool is_linear_ordered_comm_ring(type_context * tctx_ptr = nullptr);
-    bool is_field(type_context * tctx_ptr = nullptr);
-    bool is_discrete_field(type_context * tctx_ptr = nullptr);
-    optional<mpz> has_cyclic_numerals(type_context * tctx_ptr = nullptr);
-
-    expr get_zero(type_context * tctx_ptr = nullptr);
-    expr get_one(type_context * tctx_ptr = nullptr);
-    expr get_bit0(type_context * tctx_ptr = nullptr);
-    expr get_bit1(type_context * tctx_ptr = nullptr);
-    expr get_add(type_context * tctx_ptr = nullptr);
-    expr get_mul(type_context * tctx_ptr = nullptr);
-    expr get_sub(type_context * tctx_ptr = nullptr);
-    expr get_div(type_context * tctx_ptr = nullptr);
-    expr get_neg(type_context * tctx_ptr = nullptr);
-    expr get_le(type_context * tctx_ptr = nullptr);
-    expr get_lt(type_context * tctx_ptr = nullptr);
-};
-
-typedef std::shared_ptr<arith_instance_info> arith_instance_info_ref;
-
-enum class concrete_arith_type { NAT, INT, REAL };
-optional<concrete_arith_type> is_concrete_arith_type(expr const & type);
-
-arith_instance_info_ref get_arith_instance_info_for(concrete_arith_type type);
-arith_instance_info_ref get_arith_instance_info_for(type_context & tctx, expr const & type);
-
-void initialize_arith_instance_manager();
-void finalize_arith_instance_manager();
-
-}
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 582f253bb0..0e2bf2468d 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -99,6 +99,7 @@ name const * g_gt = nullptr;
 name const * g_has_add = nullptr;
 name const * g_has_div = nullptr;
 name const * g_has_mul = nullptr;
+name const * g_has_inv = nullptr;
 name const * g_has_le = nullptr;
 name const * g_has_lt = nullptr;
 name const * g_has_neg = nullptr;
@@ -171,6 +172,7 @@ name const * g_int_ne_neg_of_pos = nullptr;
 name const * g_int_neg_ne_zero_of_ne = nullptr;
 name const * g_int_zero_ne_neg_of_ne = nullptr;
 name const * g_int_decidable_linear_ordered_comm_group = nullptr;
+name const * g_inv = nullptr;
 name const * g_io = nullptr;
 name const * g_io_functor = nullptr;
 name const * g_io_monad = nullptr;
@@ -584,6 +586,7 @@ void initialize_constants() {
     g_has_add = new name{"has_add"};
     g_has_div = new name{"has_div"};
     g_has_mul = new name{"has_mul"};
+    g_has_inv = new name{"has_inv"};
     g_has_le = new name{"has_le"};
     g_has_lt = new name{"has_lt"};
     g_has_neg = new name{"has_neg"};
@@ -656,6 +659,7 @@ void initialize_constants() {
     g_int_neg_ne_zero_of_ne = new name{"int", "neg_ne_zero_of_ne"};
     g_int_zero_ne_neg_of_ne = new name{"int", "zero_ne_neg_of_ne"};
     g_int_decidable_linear_ordered_comm_group = new name{"int_decidable_linear_ordered_comm_group"};
+    g_inv = new name{"inv"};
     g_io = new name{"io"};
     g_io_functor = new name{"io", "functor"};
     g_io_monad = new name{"io", "monad"};
@@ -1070,6 +1074,7 @@ void finalize_constants() {
     delete g_has_add;
     delete g_has_div;
     delete g_has_mul;
+    delete g_has_inv;
     delete g_has_le;
     delete g_has_lt;
     delete g_has_neg;
@@ -1142,6 +1147,7 @@ void finalize_constants() {
     delete g_int_neg_ne_zero_of_ne;
     delete g_int_zero_ne_neg_of_ne;
     delete g_int_decidable_linear_ordered_comm_group;
+    delete g_inv;
     delete g_io;
     delete g_io_functor;
     delete g_io_monad;
@@ -1555,6 +1561,7 @@ name const & get_gt_name() { return *g_gt; }
 name const & get_has_add_name() { return *g_has_add; }
 name const & get_has_div_name() { return *g_has_div; }
 name const & get_has_mul_name() { return *g_has_mul; }
+name const & get_has_inv_name() { return *g_has_inv; }
 name const & get_has_le_name() { return *g_has_le; }
 name const & get_has_lt_name() { return *g_has_lt; }
 name const & get_has_neg_name() { return *g_has_neg; }
@@ -1627,6 +1634,7 @@ name const & get_int_ne_neg_of_pos_name() { return *g_int_ne_neg_of_pos; }
 name const & get_int_neg_ne_zero_of_ne_name() { return *g_int_neg_ne_zero_of_ne; }
 name const & get_int_zero_ne_neg_of_ne_name() { return *g_int_zero_ne_neg_of_ne; }
 name const & get_int_decidable_linear_ordered_comm_group_name() { return *g_int_decidable_linear_ordered_comm_group; }
+name const & get_inv_name() { return *g_inv; }
 name const & get_io_name() { return *g_io; }
 name const & get_io_functor_name() { return *g_io_functor; }
 name const & get_io_monad_name() { return *g_io_monad; }
diff --git a/src/library/constants.h b/src/library/constants.h
index aea36c925f..e8292445f7 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -101,6 +101,7 @@ name const & get_gt_name();
 name const & get_has_add_name();
 name const & get_has_div_name();
 name const & get_has_mul_name();
+name const & get_has_inv_name();
 name const & get_has_le_name();
 name const & get_has_lt_name();
 name const & get_has_neg_name();
@@ -173,6 +174,7 @@ name const & get_int_ne_neg_of_pos_name();
 name const & get_int_neg_ne_zero_of_ne_name();
 name const & get_int_zero_ne_neg_of_ne_name();
 name const & get_int_decidable_linear_ordered_comm_group_name();
+name const & get_inv_name();
 name const & get_io_name();
 name const & get_io_functor_name();
 name const & get_io_monad_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index bf1e6ed504..eed0f16ed4 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -94,6 +94,7 @@ gt
 has_add
 has_div
 has_mul
+has_inv
 has_le
 has_lt
 has_neg
@@ -166,6 +167,7 @@ int.ne_neg_of_pos
 int.neg_ne_zero_of_ne
 int.zero_ne_neg_of_ne
 int_decidable_linear_ordered_comm_group
+inv
 io
 io.functor
 io.monad
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index e41777beeb..aa178fcd03 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -44,7 +44,6 @@ Author: Leonardo de Moura
 #include "library/app_builder.h"
 #include "library/fun_info.h"
 #include "library/mpq_macro.h"
-#include "library/arith_instance_manager.h"
 #include "library/inverse.h"
 #include "library/pattern_attribute.h"
 #include "library/comp_val.h"
@@ -106,7 +105,6 @@ void initialize_library_module() {
     initialize_type_context();
     initialize_delayed_abstraction();
     initialize_mpq_macro();
-    initialize_arith_instance_manager();
     initialize_inverse();
     initialize_pattern_attribute();
     initialize_comp_val();
@@ -124,7 +122,6 @@ void finalize_library_module() {
     finalize_comp_val();
     finalize_pattern_attribute();
     finalize_inverse();
-    finalize_arith_instance_manager();
     finalize_mpq_macro();
     finalize_delayed_abstraction();
     finalize_type_context();
diff --git a/src/library/mpq_macro.cpp b/src/library/mpq_macro.cpp
index b2b80b4540..fd2dae7d04 100644
--- a/src/library/mpq_macro.cpp
+++ b/src/library/mpq_macro.cpp
@@ -13,19 +13,19 @@ Author: Daniel Selsam
 #include "library/constants.h"
 #include "library/kernel_serializer.h"
 #include "library/type_context.h"
-#include "library/arith_instance_manager.h"
+#include "library/arith_instance.h"
 
 namespace lean {
 
 struct mpq2expr_fn {
-    arith_instance_info_ref m_info;
+    arith_instance & m_ainst;
 
-    mpq2expr_fn(arith_instance_info_ref info): m_info(info) {}
+    mpq2expr_fn(arith_instance & ainst): m_ainst(ainst) {}
 
     expr operator()(mpq const & q) {
         mpz numer = q.get_numerator();
         if (numer.is_zero())
-            return m_info->get_zero();
+            return m_ainst.mk_zero();
 
         mpz denom = q.get_denominator();
         lean_assert(denom > 0);
@@ -40,11 +40,11 @@ struct mpq2expr_fn {
         if (denom == 1) {
             e = pos_mpz_to_expr(numer);
         } else {
-            e = mk_app(m_info->get_div(), pos_mpz_to_expr(numer), pos_mpz_to_expr(denom));
+            e = mk_app(m_ainst.mk_div(), pos_mpz_to_expr(numer), pos_mpz_to_expr(denom));
         }
 
         if (flip_sign) {
-            return mk_app(m_info->get_neg(), e);
+            return mk_app(m_ainst.mk_neg(), e);
         } else {
             return e;
         }
@@ -53,11 +53,11 @@ struct mpq2expr_fn {
     expr pos_mpz_to_expr(mpz const & n) {
         lean_assert(n > 0);
         if (n == 1)
-            return m_info->get_one();
+            return m_ainst.mk_one();
         if (n % mpz(2) == 1)
-            return mk_app(m_info->get_bit1(), pos_mpz_to_expr(n/2));
+            return mk_app(m_ainst.mk_bit1(), pos_mpz_to_expr(n/2));
         else
-            return mk_app(m_info->get_bit0(), pos_mpz_to_expr(n/2));
+            return mk_app(m_ainst.mk_bit0(), pos_mpz_to_expr(n/2));
     }
 };
 
@@ -86,20 +86,14 @@ public:
         return macro_arg(m, 0);
     }
 
-    virtual optional<expr> expand(expr const & m, abstract_type_context &) const {
+    virtual optional<expr> expand(expr const & m, abstract_type_context & actx) const {
         check_macro(m);
-        expr ty = macro_arg(m, 0);
-        concrete_arith_type cty;
-        if (ty == mk_constant(get_nat_name()))
-            cty = concrete_arith_type::NAT;
-        else if (ty == mk_constant(get_int_name()))
-            cty = concrete_arith_type::INT;
-        else if (ty == mk_constant(get_real_name()))
-            cty = concrete_arith_type::REAL;
-        else
+        expr type = macro_arg(m, 0);
+        if (has_local(type) || has_metavar(type))
             throw exception(sstream() << "trying to expand invalid 'mpq' macro");
-
-        return some_expr(mpq2expr_fn(get_arith_instance_info_for(cty))(get_mpq()));
+        type_context ctx(actx.env());
+        arith_instance ainst(ctx, type);
+        return some_expr(mpq2expr_fn(ainst)(m_q));
     }
 
     virtual void write(serializer & s) const {