diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index d23991e4b6..1c28808726 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -480,7 +480,7 @@ class elaborator::imp {
     }
 
     bool is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) {
-        if (is_app(e1) && is_meta(arg(e1,0)) && is_var(arg(e1,1), 0) && num_args(e1) == 2 && !is_empty(ctx)) {
+        if (is_app(e1) && is_meta(arg(e1, 0)) && is_var(arg(e1, 1), 0) && num_args(e1) == 2 && !is_empty(ctx)) {
             return true;
         } else {
             return false;
@@ -490,7 +490,7 @@ class elaborator::imp {
     void unify_simple_ho_match(expr const & e1, expr const & e2, constraint const & c) {
         context const & ctx = c.m_ctx;
         context_entry const & head = ::lean::lookup(ctx, 0);
-        m_constraints.push_back(constraint(arg(e1,0), mk_lambda(head.get_name(),
+        m_constraints.push_back(constraint(arg(e1, 0), mk_lambda(head.get_name(),
                                                            lift_free_vars_mmv(head.get_domain(), 1, 1),
                                                            lift_free_vars_mmv(e2, 1, 1)), c));
     }
@@ -882,7 +882,7 @@ void elaborator::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
 void elaborator::clear() { m_ptr->clear(); }
 environment const & elaborator::get_environment() const { return m_ptr->get_environment(); }
 void elaborator::display(std::ostream & out) const { m_ptr->display(out); }
-format elaborator::pp(formatter & f, options const & o) const { return m_ptr->pp(f,o); }
+format elaborator::pp(formatter & f, options const & o) const { return m_ptr->pp(f, o); }
 void elaborator::print(imp * ptr) { ptr->display(std::cout); }
 bool elaborator::has_constraints() const { return m_ptr->has_constraints(); }
 }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index b7a7c31921..c225375b49 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1423,7 +1423,7 @@ class parser::imp {
                                 << "  Eval [expr]            evaluate the given expression" << endl
                                 << "  Help                   display this message" << endl
                                 << "  Help Options           display available options" << endl
-                                << "  Help Notation          describe commands for defining infix,mixfix,postfix operators" << endl
+                                << "  Help Notation          describe commands for defining infix, mixfix, postfix operators" << endl
                                 << "  Import [string]        load the given file" << endl
                                 << "  Set [id] [value]       set option [id] with value [value]" << endl
                                 << "  Show [expr]            pretty print the given expression" << endl
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 7eda10c288..edd5236161 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -174,7 +174,7 @@ class pp_fn {
     typedef std::pair<format, unsigned> result;
 
     bool is_coercion(expr const & e) {
-        return is_app(e) && num_args(e) == 2 && m_frontend.is_coercion(arg(e,0));
+        return is_app(e) && num_args(e) == 2 && m_frontend.is_coercion(arg(e, 0));
     }
 
     /**
@@ -186,7 +186,7 @@ class pp_fn {
             return true;
         case expr_kind::App:
             if (!m_coercion && is_coercion(e))
-                return is_atomic(arg(e,1));
+                return is_atomic(arg(e, 1));
             else
                 return false;
         case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Eq: case expr_kind::Let:
@@ -490,7 +490,7 @@ class pp_fn {
 
         application(expr const & e, pp_fn const & owner, bool show_implicit):m_app(e) {
             frontend const & fe = owner.m_frontend;
-            expr const & f = arg(e,0);
+            expr const & f = arg(e, 0);
             if (is_constant(f) && owner.has_implicit_arguments(const_name(f))) {
                 m_implicit_args = &(fe.get_implicit_arguments(const_name(f)));
                 if (show_implicit || num_args(e) - 1 < m_implicit_args->size()) {
@@ -594,7 +594,7 @@ class pp_fn {
     */
     result pp_app(expr const & e, unsigned depth) {
         if (!m_coercion && is_coercion(e))
-            return pp(arg(e,1), depth);
+            return pp(arg(e, 1), depth);
         application app(e, *this, m_implict);
         operator_info op;
         if (m_notation && app.notation_enabled() && (op = get_operator(e)) && has_expected_num_args(app, op)) {
@@ -668,7 +668,7 @@ class pp_fn {
         } else {
             // standard function application
             expr const & f  = app.get_function();
-            result p        = is_constant(f) && !is_metavar(f) ? mk_result(format(const_name(f)),1) : pp_child(f, depth);
+            result p        = is_constant(f) && !is_metavar(f) ? mk_result(format(const_name(f)), 1) : pp_child(f, depth);
             bool simple     = is_constant(f) && !is_metavar(f) && const_name(f).size() <= m_indent + 4;
             unsigned indent = simple ? const_name(f).size()+1 : m_indent;
             format   r_format = p.first;
diff --git a/src/interval/interval.h b/src/interval/interval.h
index 44c55615a5..b61a25adef 100644
--- a/src/interval/interval.h
+++ b/src/interval/interval.h
@@ -73,18 +73,18 @@ public:
 
     // (-oo, oo)
     interval();
-    // [n,n]
+    // [n, n]
     template<typename T2> interval(T2 const & n):m_lower(n), m_upper(n) { set_closed_endpoints();}
     // copy constructor
     interval(interval<T> const & n);
     // move constructor
     interval(interval<T> && src);
 
-    // [l,u], (l,u], [l,u), (l,u)
+    // [l, u], (l, u], [l, u), (l, u)
     template<typename T2> interval(T2 const & l, T2 const & u, bool l_open = false, bool u_open = false):m_lower(l), m_upper(u) {
         m_lower_open = l_open; m_upper_open = u_open; m_lower_inf  = false; m_upper_inf  = false;
     }
-    // [l,u], (l,u], [l,u), (l,u)
+    // [l, u], (l, u], [l, u), (l, u)
     template<typename T2> interval(bool l_open, T2 const & l, T2 const & u, bool u_open):interval(l, u, l_open, u_open) {}
     // (-oo, u], (-oo, u]
     template<typename T2> interval(T2 const & u, bool u_open):m_upper(u) {
@@ -129,7 +129,7 @@ public:
     bool is_N1() const { return is_upper_neg() || (is_upper_zero() && is_upper_open()); }
     // lower is negative and upper is positive
     bool is_M() const { return is_lower_neg() && is_upper_pos(); }
-    // [0,0]
+    // [0, 0]
     bool is_zero() const { return is_lower_zero() && is_upper_zero(); }
 
     // Interval contains the value zero
diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h
index 04064de5f2..cea18ba960 100644
--- a/src/interval/interval_def.h
+++ b/src/interval/interval_def.h
@@ -878,7 +878,7 @@ template<typename T> void interval<T>::inv_jst(interval_deps & deps) {
 template<typename T>
 template<bool compute_intv, bool compute_deps>
 void interval<T>::inv(interval_deps & deps) {
-    // If the interval [l,u] does not contain 0, then 1/[l,u] = [1/u, 1/l]
+    // If the interval [l, u] does not contain 0, then 1/[l, u] = [1/u, 1/l]
     lean_assert(!contains_zero());
 
     using std::swap;
@@ -2175,7 +2175,7 @@ void interval<T>::cosh (interval_deps & deps) {
                 lean_assert(check_invariant());
             }
             if(compute_deps) {
-                // cos([a,b]) = [cosh(a), cos(b)]
+                // cos([a, b]) = [cosh(a), cos(b)]
                 deps.m_lower_deps = DEP_IN_LOWER1;
                 deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1;
             }
@@ -2197,7 +2197,7 @@ void interval<T>::cosh (interval_deps & deps) {
             }
             return;
         }
-        // [a,b] where a < 0 < b
+        // [a, b] where a < 0 < b
         if(m_lower + m_upper < 0.0) {
             if(compute_intv) {
                 m_upper = m_lower;
@@ -2247,7 +2247,7 @@ void interval<T>::cosh (interval_deps & deps) {
         }
     }
     if(upper_kind() == XN_NUMERAL) {
-        // [-oo,c]
+        // [-oo, c]
         lean_assert(lower_kind() == XN_MINUS_INFINITY);
         if(compute_intv) {
             m_upper_inf = true;
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index db0685d2d7..30e3ac486d 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -204,10 +204,10 @@ void import_basic(environment & env) {
     // forall : Pi (A : Type u), (A -> Bool) -> Bool
     env.add_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True))));
     // TODO(Leo): introduce epsilon
-    env.add_definition(exists_fn_name, q_type, Fun({{A,TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
+    env.add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
 
     // homogeneous equality
-    env.add_definition(homo_eq_fn_name, Pi({{A,TypeU},{x,A},{y,A}}, Bool), Fun({{A,TypeU}, {x,A}, {y,A}}, Eq(x, y)));
+    env.add_definition(homo_eq_fn_name, Pi({{A, TypeU}, {x, A}, {y, A}}, Bool), Fun({{A, TypeU}, {x, A}, {y, A}}, Eq(x, y)));
 
     // MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b
     env.add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b));
@@ -222,7 +222,7 @@ void import_basic(environment & env) {
     env.add_axiom(case_fn_name, Pi({{P, Bool >> Bool}, {H1, P(True)}, {H2, P(False)}, {a, Bool}}, P(a)));
 
     // Subst : Pi (A : Type u) (a b : A) (P : A -> bool) (H1 : P a) (H2 : a = b), P b
-    env.add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a,b)}}, P(b)));
+    env.add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a, b)}}, P(b)));
 
     // Eta : Pi (A : Type u) (B : A -> Type u), f : (Pi x : A, B x), (Fun x : A => f x) = f
     env.add_axiom(eta_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}}, Eq(Fun({x, A}, f(x)), f)));
diff --git a/src/kernel/context.h b/src/kernel/context.h
index 937b752be3..cbca17583d 100644
--- a/src/kernel/context.h
+++ b/src/kernel/context.h
@@ -34,8 +34,8 @@ class context {
     explicit context(list<context_entry> const & l):m_list(l) {}
 public:
     context() {}
-    context(context const & c, name const & n, expr const & d):m_list(context_entry(n,d), c.m_list) {}
-    context(context const & c, name const & n, expr const & d, expr const & b):m_list(context_entry(n,d,b), c.m_list) {}
+    context(context const & c, name const & n, expr const & d):m_list(context_entry(n, d), c.m_list) {}
+    context(context const & c, name const & n, expr const & d, expr const & b):m_list(context_entry(n, d, b), c.m_list) {}
     context_entry const & lookup(unsigned vidx) const;
     std::pair<context_entry const &, context> lookup_ext(unsigned vidx) const;
     bool is_empty() const { return is_nil(m_list); }
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 3d8ead848b..5e21de0fbc 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -30,7 +30,7 @@ class value;
           |   Eq            expr expr         (heterogeneous equality)
           |   Let           name expr expr expr
 
-TODO: match expressions.
+TODO(Leo): match expressions.
 
 The main API is divided in the following sections
 - Testers
@@ -386,11 +386,11 @@ struct expr_eqp { bool operator()(expr const & e1, expr const & e2) const { retu
 struct expr_cell_hash { unsigned operator()(expr_cell * e) const { return e->hash(); } };
 /** \brief Functional object for testing pointer equality between kernel cell expressions. */
 struct expr_cell_eqp { bool operator()(expr_cell * e1, expr_cell * e2) const { return e1 == e2; } };
-/** \brief Functional object for hashing a pair (n,k) where n is a kernel expressions, and k is an offset. */
+/** \brief Functional object for hashing a pair (n, k) where n is a kernel expressions, and k is an offset. */
 struct expr_offset_hash { unsigned operator()(expr_offset const & p) const { return hash(p.first.hash(), p.second); } };
 /** \brief Functional object for comparing pairs (expression, offset). */
 struct expr_offset_eqp { unsigned operator()(expr_offset const & p1, expr_offset const & p2) const { return is_eqp(p1.first, p2.first) && p1.second == p2.second; } };
-/** \brief Functional object for hashing a pair (n,k) where n is a kernel cell expressions, and k is an offset. */
+/** \brief Functional object for hashing a pair (n, k) where n is a kernel cell expressions, and k is an offset. */
 struct expr_cell_offset_hash { unsigned operator()(expr_cell_offset const & p) const { return hash(p.first->hash(), p.second); } };
 /** \brief Functional object for comparing pairs (expression cell, offset). */
 struct expr_cell_offset_eqp { unsigned operator()(expr_cell_offset const & p1, expr_cell_offset const & p2) const { return p1 == p2; } };
diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h
index 94ad566532..0ac9a20a4b 100644
--- a/src/kernel/instantiate.h
+++ b/src/kernel/instantiate.h
@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 /**
-   \brief Replace the free variables with indices 0,...,n-1 with s[n-1],...,s[0] in e.
+   \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e.
 
    \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables).
 */
@@ -17,7 +17,7 @@ expr instantiate_with_closed(expr const & e, unsigned n, expr const * s);
 inline expr instantiate_with_closed(expr const & e, expr const & s) { return instantiate_with_closed(e, 1, &s); }
 
 /**
-   \brief Replace the free variables with indices 0,...,n-1 with s[n-1],...,s[0] in e.
+   \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e.
 */
 expr instantiate(expr const & e, unsigned n, expr const * s);
 inline expr instantiate(expr const & e, expr const & s) { return instantiate(e, 1, &s); }
diff --git a/src/library/arith/special_fn.cpp b/src/library/arith/special_fn.cpp
index cb411f4c7e..c3952813ea 100644
--- a/src/library/arith/special_fn.cpp
+++ b/src/library/arith/special_fn.cpp
@@ -42,19 +42,19 @@ void import_special_fn(environment & env) {
     env.add_var(real_pi_name, Real);
     env.add_definition(name("pi"), Real, mk_real_pi()); // alias for pi
     env.add_var(sin_fn_name, r_r);
-    env.add_definition(cos_fn_name, r_r, Fun({x,Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2))))));
-    env.add_definition(tan_fn_name, r_r, Fun({x,Real}, rDiv(Sin(x), Cos(x))));
-    env.add_definition(cot_fn_name, r_r, Fun({x,Real}, rDiv(Cos(x), Sin(x))));
-    env.add_definition(sec_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cos(x))));
-    env.add_definition(csc_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sin(x))));
+    env.add_definition(cos_fn_name, r_r, Fun({x, Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2))))));
+    env.add_definition(tan_fn_name, r_r, Fun({x, Real}, rDiv(Sin(x), Cos(x))));
+    env.add_definition(cot_fn_name, r_r, Fun({x, Real}, rDiv(Cos(x), Sin(x))));
+    env.add_definition(sec_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cos(x))));
+    env.add_definition(csc_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sin(x))));
 
     env.add_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))),
                                                               rMul(rVal(2), Exp(rNeg(x))))));
     env.add_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))),
                                                               rMul(rVal(2), Exp(rNeg(x))))));
-    env.add_definition(tanh_fn_name, r_r, Fun({x,Real}, rDiv(Sinh(x), Cosh(x))));
-    env.add_definition(coth_fn_name, r_r, Fun({x,Real}, rDiv(Cosh(x), Sinh(x))));
-    env.add_definition(sech_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cosh(x))));
-    env.add_definition(csch_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sinh(x))));
+    env.add_definition(tanh_fn_name, r_r, Fun({x, Real}, rDiv(Sinh(x), Cosh(x))));
+    env.add_definition(coth_fn_name, r_r, Fun({x, Real}, rDiv(Cosh(x), Sinh(x))));
+    env.add_definition(sech_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cosh(x))));
+    env.add_definition(csch_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sinh(x))));
 }
 }
diff --git a/src/library/basic_thms.cpp b/src/library/basic_thms.cpp
index fa129a45e3..9f0fe66243 100644
--- a/src/library/basic_thms.cpp
+++ b/src/library/basic_thms.cpp
@@ -184,9 +184,9 @@ void import_basic_thms(environment & env) {
                                                 Discharge(Not(b), a, Fun({H1, Not(b)},
                                                                          FalseElim(a, Absurd(b, H, H1))))))));
 
-    // DisjCases : Pi (a b c: Bool) (H1 : Or(a,b)) (H2 : a -> c) (H3 : b -> c), c */
-    env.add_theorem(disj_cases_fn_name, Pi({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a,b)}, {H2, a >> c}, {H3, b >> c}}, c),
-                    Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a,b)}, {H2, a >> c}, {H3, b >> c}},
+    // DisjCases : Pi (a b c: Bool) (H1 : Or(a, b)) (H2 : a -> c) (H3 : b -> c), c */
+    env.add_theorem(disj_cases_fn_name, Pi({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}}, c),
+                    Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}},
                         EqMP(Not(Not(c)), c, DoubleNeg(c),
                              Discharge(Not(c), False,
                                        Fun({H, Not(c)},
@@ -200,11 +200,11 @@ void import_basic_thms(environment & env) {
     // Symm : Pi (A : Type u) (a b : A) (H : a = b), b = a
     env.add_theorem(symm_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(b, a)),
                     Fun({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}},
-                        Subst(A, a, b, Fun({x, A}, Eq(x,a)), Refl(A, a), H)));
+                        Subst(A, a, b, Fun({x, A}, Eq(x, a)), Refl(A, a), H)));
 
     // Trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c
     env.add_theorem(trans_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
-                    Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a,b)}, {H2, Eq(b,c)}},
+                    Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
                         Subst(A, b, c, Fun({x, A}, Eq(a, x)), H1, H2)));
 
     // TransExt: Pi (A: Type u) (B : Type u) (a : A) (b c : B) (H1 : a = b) (H2 : b = c), a = c
diff --git a/src/library/basic_thms.h b/src/library/basic_thms.h
index 58dfb9b96c..c3c3295483 100644
--- a/src/library/basic_thms.h
+++ b/src/library/basic_thms.h
@@ -81,7 +81,7 @@ expr mk_disj2_fn();
 inline expr Disj2(expr const & b, expr const & a, expr const & H) { return mk_app(mk_disj2_fn(), b, a, H); }
 
 expr mk_disj_cases_fn();
-/** \brief (Theorem) {a b c : Bool}, H1 : Or(a,b), H2 : a -> c, H3 : b -> c |- DisjCases(a, b, c, H1, H2, H3) : c */
+/** \brief (Theorem) {a b c : Bool}, H1 : Or(a, b), H2 : a -> c, H3 : b -> c |- DisjCases(a, b, c, H1, H2, H3) : c */
 inline expr DisjCases(expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2, expr const & H3) { return mk_app({mk_disj_cases_fn(), a, b, c, H1, H2, H3}); }
 
 expr mk_symm_fn();
diff --git a/src/library/cast/cast.cpp b/src/library/cast/cast.cpp
index 48ee152e60..2820e94387 100644
--- a/src/library/cast/cast.cpp
+++ b/src/library/cast/cast.cpp
@@ -22,7 +22,7 @@ public:
         expr A    = Const("A");
         expr B    = Const("B");
         // Cast: Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B
-        m_type = Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B));
+        m_type = Pi({{A, TypeU}, {B, TypeU}}, Eq(A, B) >> (A >> B));
     }
     virtual ~cast_fn_value() {}
     virtual expr get_type() const { return m_type; }
@@ -122,7 +122,7 @@ void import_cast(environment & env) {
 
     // Alias for Cast operator. We create the alias to be able to mark
     // implicit arguments.
-    env.add_definition(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B)), mk_Cast_fn());
+    env.add_definition(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A, B) >> (A >> B)), mk_Cast_fn());
 
     // DomInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A'
     env.add_axiom(dom_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}}, Eq(A, Ap)));
diff --git a/src/library/context_to_lambda.cpp b/src/library/context_to_lambda.cpp
index 9680263cab..f1466a97c6 100644
--- a/src/library/context_to_lambda.cpp
+++ b/src/library/context_to_lambda.cpp
@@ -25,7 +25,7 @@ expr context_to_lambda(context const & c, expr const & e) {
     return context_to_lambda(c.begin(), c.end(), e);
 }
 bool is_fake_context(expr const & e) {
-    return is_lambda(e) && is_app(abst_domain(e)) && arg(abst_domain(e),0) == g_fake;
+    return is_lambda(e) && is_app(abst_domain(e)) && arg(abst_domain(e), 0) == g_fake;
 }
 name const & fake_context_name(expr const & e) {
     lean_assert(is_fake_context(e));
diff --git a/src/library/formatter.cpp b/src/library/formatter.cpp
index a773f0a313..975d728e41 100644
--- a/src/library/formatter.cpp
+++ b/src/library/formatter.cpp
@@ -22,7 +22,7 @@ public:
         std::ostringstream s;
         if (format_ctx)
             s << c << "|-\n";
-        s << mk_pair(e,c);
+        s << mk_pair(e, c);
         return format(s.str());
     }
     virtual format operator()(object const & obj, options const & opts) {
diff --git a/src/library/metavar.cpp b/src/library/metavar.cpp
index bb5fccb3ab..4e022ebc40 100644
--- a/src/library/metavar.cpp
+++ b/src/library/metavar.cpp
@@ -319,11 +319,11 @@ static expr get_def_value(name const & n, environment const & env, name_set cons
 
 expr head_reduce_mmv(expr const & e, environment const & env, name_set const * defs) {
     if (is_app(e) && is_lambda(arg(e, 0))) {
-        expr r = arg(e,0);
+        expr r = arg(e, 0);
         unsigned num = num_args(e);
         unsigned i = 1;
         while (i < num) {
-            r = instantiate_free_var_mmv(abst_body(r), 0, arg(e,i));
+            r = instantiate_free_var_mmv(abst_body(r), 0, arg(e, i));
             i = i + 1;
             if (!is_lambda(r))
                 break;
@@ -332,7 +332,7 @@ expr head_reduce_mmv(expr const & e, environment const & env, name_set const * d
             buffer<expr> args;
             args.push_back(r);
             for (; i < num; i++)
-                args.push_back(arg(e,i));
+                args.push_back(arg(e, i));
             r = mk_app(args.size(), args.data());
         }
         return r;
diff --git a/src/tests/frontends/lean/implicit_args.cpp b/src/tests/frontends/lean/implicit_args.cpp
index bd5c2f2acd..61ad4ee495 100644
--- a/src/tests/frontends/lean/implicit_args.cpp
+++ b/src/tests/frontends/lean/implicit_args.cpp
@@ -81,9 +81,9 @@ static void tst1() {
     env.add_var("F", Pi({{A, Type()}, {B, Type()}, {g, A >> B}}, A));
     env.add_var("f", Nat >> Real);
     expr f = Const("f");
-    success(F(_,_,f), F(Nat, Real, f), env);
-    // fails(F(_,Bool,f), env);
-    success(F(_,_,Fun({a, Nat},a)), F(Nat,Nat,Fun({a,Nat},a)), env);
+    success(F(_, _, f), F(Nat, Real, f), env);
+    // fails(F(_, Bool, f), env);
+    success(F(_, _, Fun({a, Nat}, a)), F(Nat, Nat, Fun({a, Nat}, a)), env);
 }
 
 static void tst2() {
@@ -98,15 +98,15 @@ static void tst2() {
     env.add_var("c", Bool);
     env.add_axiom("H1", Eq(a, b));
     env.add_axiom("H2", Eq(b, c));
-    success(Trans(_,_,_,_,H1,H2), Trans(Bool,a,b,c,H1,H2), env);
-    success(Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1)),
-            Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1)), env);
-    success(Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1))),
-            Symm(Bool,c,a,Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1))), env);
+    success(Trans(_, _, _, _, H1, H2), Trans(Bool, a, b, c, H1, H2), env);
+    success(Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1)),
+            Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1)), env);
+    success(Symm(_, _, _, Trans(_, _ , _ , _ , Symm(_, _, _, H2), Symm(_, _, _, H1))),
+            Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), env);
     env.add_axiom("H3", a);
     expr H3 = Const("H3");
-    success(EqTIntro(_, EqMP(_,_,Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1))), H3)),
-            EqTIntro(c, EqMP(a,c,Symm(Bool,c,a,Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1))), H3)),
+    success(EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3)),
+            EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3)),
             env);
 }
 
@@ -127,17 +127,17 @@ static void tst3() {
     env.add_var("b", Nat);
     env.add_definition("fact", Bool, Eq(a, b));
     env.add_axiom("H", fact);
-    success(Congr2(_,_,_,_,f,H),
-            Congr2(Nat, Fun({n,Nat}, vec(n) >> Nat), a, b, f, H), env);
+    success(Congr2(_, _, _, _, f, H),
+            Congr2(Nat, Fun({n, Nat}, vec(n) >> Nat), a, b, f, H), env);
     env.add_var("g", Pi({n, Nat}, vec(n) >> Nat));
     expr g = Const("g");
     env.add_axiom("H2", Eq(f, g));
     expr H2 = Const("H2");
-    success(Congr(_,_,_,_,_,_,H2,H),
-            Congr(Nat, Fun({n,Nat}, vec(n) >> Nat), f, g, a, b, H2, H), env);
-    success(Congr(_,_,_,_,_,_,Refl(_,f),H),
-            Congr(Nat, Fun({n,Nat}, vec(n) >> Nat), f, f, a, b, Refl(Pi({n, Nat}, vec(n) >> Nat),f), H), env);
-    success(Refl(_,a), Refl(Nat,a), env);
+    success(Congr(_, _, _, _, _, _, H2, H),
+            Congr(Nat, Fun({n, Nat}, vec(n) >> Nat), f, g, a, b, H2, H), env);
+    success(Congr(_, _, _, _, _, _, Refl(_, f), H),
+            Congr(Nat, Fun({n, Nat}, vec(n) >> Nat), f, f, a, b, Refl(Pi({n, Nat}, vec(n) >> Nat), f), H), env);
+    success(Refl(_, a), Refl(Nat, a), env);
 }
 
 static void tst4() {
@@ -153,13 +153,13 @@ static void tst4() {
     expr x   = Const("x");
     expr y   = Const("y");
     expr z   = Const("z");
-    success(Fun({{x,_},{y,_}}, f(x, y)),
-            Fun({{x,Nat},{y,R >> Nat}}, f(x, y)), env);
-    success(Fun({{x,_},{y,_},{z,_}}, Eq(f(x, y), f(x, z))),
-            Fun({{x,Nat},{y,R >> Nat},{z,R >> Nat}}, Eq(f(x, y), f(x, z))), env);
+    success(Fun({{x, _}, {y, _}}, f(x, y)),
+            Fun({{x, Nat}, {y, R >> Nat}}, f(x, y)), env);
+    success(Fun({{x, _}, {y, _}, {z, _}}, Eq(f(x, y), f(x, z))),
+            Fun({{x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, Eq(f(x, y), f(x, z))), env);
     expr A   = Const("A");
-    success(Fun({{A,Type()},{x,_},{y,_},{z,_}}, Eq(f(x, y), f(x, z))),
-            Fun({{A,Type()},{x,Nat},{y,R >> Nat},{z,R >> Nat}}, Eq(f(x, y), f(x, z))), env);
+    success(Fun({{A, Type()}, {x, _}, {y, _}, {z, _}}, Eq(f(x, y), f(x, z))),
+            Fun({{A, Type()}, {x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, Eq(f(x, y), f(x, z))), env);
 }
 
 static void tst5() {
@@ -172,10 +172,10 @@ static void tst5() {
     expr g = Const("g");
     expr Nat = Const("N");
     env.add_var("N", Type());
-    env.add_var("f", Pi({{A,Type()},{a,A},{b,A}}, A));
+    env.add_var("f", Pi({{A, Type()}, {a, A}, {b, A}}, A));
     env.add_var("g", Nat >> Nat);
-    success(Fun({{a,_},{b,_}},g(f(_,a,b))),
-            Fun({{a,Nat},{b,Nat}},g(f(Nat,a,b))), env);
+    success(Fun({{a, _}, {b, _}}, g(f(_, a, b))),
+            Fun({{a, Nat}, {b, Nat}}, g(f(Nat, a, b))), env);
 }
 
 static void tst6() {
@@ -193,14 +193,14 @@ static void tst6() {
     env.add_var("nil", Pi({A, Type()}, lst(A)));
     env.add_var("cons", Pi({{A, Type()}, {a, A}, {l, lst(A)}}, lst(A)));
     env.add_var("f", lst(N>>N) >> Bool);
-    success(Fun({a,_}, f(cons(_, a, cons(_, a, nil(_))))),
-            Fun({a,N>>N}, f(cons(N>>N, a, cons(N>>N, a, nil(N>>N))))), env);
+    success(Fun({a, _}, f(cons(_, a, cons(_, a, nil(_))))),
+            Fun({a, N>>N}, f(cons(N>>N, a, cons(N>>N, a, nil(N>>N))))), env);
 }
 
 static void tst7() {
     frontend env;
     expr x = Const("x");
-    expr omega = mk_app(Fun({x,_}, x(x)), Fun({x,_}, x(x)));
+    expr omega = mk_app(Fun({x, _}, x(x)), Fun({x, _}, x(x)));
     fails(omega, env);
 }
 
@@ -211,18 +211,18 @@ static void tst8() {
     expr x = Const("x");
     expr f = Const("f");
     env.add_var("f", Pi({B, Type()}, B >> B));
-    success(Fun({{A,Type()}, {B,Type()}, {x,_}}, f(B, x)),
-            Fun({{A,Type()}, {B,Type()}, {x,B}}, f(B, x)), env);
-    fails(Fun({{x,_}, {A,Type()}}, f(A, x)), env);
-    success(Fun({{A,Type()}, {x,_}}, f(A, x)),
-            Fun({{A,Type()}, {x,A}}, f(A, x)), env);
-    success(Fun({{A,Type()}, {B,Type()}, {x,_}}, f(A, x)),
-            Fun({{A,Type()}, {B,Type()}, {x,A}}, f(A, x)), env);
-    success(Fun({{A,Type()}, {B,Type()}, {x,_}}, Eq(f(B, x), f(_,x))),
-            Fun({{A,Type()}, {B,Type()}, {x,B}}, Eq(f(B, x), f(B,x))), env);
-    success(Fun({{A,Type()}, {B,_}, {x,_}}, Eq(f(B, x), f(_,x))),
-            Fun({{A,Type()}, {B,Type()}, {x,B}}, Eq(f(B, x), f(B,x))), env);
-    unsolved(Fun({{A,_}, {B,_}, {x,_}}, Eq(f(B, x), f(_,x))), env);
+    success(Fun({{A, Type()}, {B, Type()}, {x, _}}, f(B, x)),
+            Fun({{A, Type()}, {B, Type()}, {x, B}}, f(B, x)), env);
+    fails(Fun({{x, _}, {A, Type()}}, f(A, x)), env);
+    success(Fun({{A, Type()}, {x, _}}, f(A, x)),
+            Fun({{A, Type()}, {x, A}}, f(A, x)), env);
+    success(Fun({{A, Type()}, {B, Type()}, {x, _}}, f(A, x)),
+            Fun({{A, Type()}, {B, Type()}, {x, A}}, f(A, x)), env);
+    success(Fun({{A, Type()}, {B, Type()}, {x, _}}, Eq(f(B, x), f(_, x))),
+            Fun({{A, Type()}, {B, Type()}, {x, B}}, Eq(f(B, x), f(B, x))), env);
+    success(Fun({{A, Type()}, {B, _}, {x, _}}, Eq(f(B, x), f(_, x))),
+            Fun({{A, Type()}, {B, Type()}, {x, B}}, Eq(f(B, x), f(B, x))), env);
+    unsolved(Fun({{A, _}, {B, _}, {x, _}}, Eq(f(B, x), f(_, x))), env);
 }
 
 static void tst9() {
@@ -234,7 +234,7 @@ static void tst9() {
     expr x = Const("x");
     expr y = Const("y");
     env.add_var("N", Type());
-    env.add_var("f", Pi({A,Type()}, A >> A));
+    env.add_var("f", Pi({A, Type()}, A >> A));
     expr N = Const("N");
     success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g(_, True, False)),
             Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g(Bool, True, False)),
@@ -247,21 +247,21 @@ static void tst9() {
             env);
     success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
                 g(_,
-                  Fun({{x,_},{y,_}}, Eq(f(_, x), f(_, y))),
-                  Fun({{x,N},{y,Bool}}, True))),
+                  Fun({{x, _}, {y, _}}, Eq(f(_, x), f(_, y))),
+                  Fun({{x, N}, {y, Bool}}, True))),
             Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
                 g((N >> (Bool >> Bool)),
-                  Fun({{x,N},{y,Bool}}, Eq(f(N, x), f(Bool, y))),
-                  Fun({{x,N},{y,Bool}}, True))), env);
+                  Fun({{x, N}, {y, Bool}}, Eq(f(N, x), f(Bool, y))),
+                  Fun({{x, N}, {y, Bool}}, True))), env);
 
     success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
                 g(_,
-                  Fun({{x,N},{y,_}}, Eq(f(_, x), f(_, y))),
-                  Fun({{x,_},{y,Bool}}, True))),
+                  Fun({{x, N}, {y, _}}, Eq(f(_, x), f(_, y))),
+                  Fun({{x, _}, {y, Bool}}, True))),
             Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
                 g((N >> (Bool >> Bool)),
-                  Fun({{x,N},{y,Bool}}, Eq(f(N, x), f(Bool, y))),
-                  Fun({{x,N},{y,Bool}}, True))), env);
+                  Fun({{x, N}, {y, Bool}}, Eq(f(N, x), f(Bool, y))),
+                  Fun({{x, N}, {y, Bool}}, True))), env);
 }
 
 static void tst10() {
@@ -273,19 +273,19 @@ static void tst10() {
     expr b = Const("b");
     expr eq = Const("eq");
     env.add_var("eq", Pi({A, Type()}, A >> (A >> Bool)));
-    success(Fun({{A, Type()},{B,Type()},{a,_},{b,B}}, eq(_,a,b)),
-            Fun({{A, Type()},{B,Type()},{a,B},{b,B}}, eq(B,a,b)), env);
-    success(Fun({{A, Type()},{B,Type()},{a,_},{b,A}}, eq(_,a,b)),
-            Fun({{A, Type()},{B,Type()},{a,A},{b,A}}, eq(A,a,b)), env);
-    success(Fun({{A, Type()},{B,Type()},{a,A},{b,_}}, eq(_,a,b)),
-            Fun({{A, Type()},{B,Type()},{a,A},{b,A}}, eq(A,a,b)), env);
-    success(Fun({{A, Type()},{B,Type()},{a,B},{b,_}}, eq(_,a,b)),
-            Fun({{A, Type()},{B,Type()},{a,B},{b,B}}, eq(B,a,b)), env);
-    success(Fun({{A, Type()},{B,Type()},{a,B},{b,_},{C,Type()}}, eq(_,a,b)),
-            Fun({{A, Type()},{B,Type()},{a,B},{b,B},{C,Type()}}, eq(B,a,b)), env);
-    fails(Fun({{A, Type()},{B,Type()},{a,_},{b,_},{C,Type()}}, eq(C,a,b)), env);
-    success(Fun({{A, Type()},{B,Type()},{a,_},{b,_},{C,Type()}}, eq(B,a,b)),
-            Fun({{A, Type()},{B,Type()},{a,B},{b,B},{C,Type()}}, eq(B,a,b)), env);
+    success(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, B}}, eq(_, a, b)),
+            Fun({{A, Type()}, {B, Type()}, {a, B}, {b, B}}, eq(B, a, b)), env);
+    success(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, A}}, eq(_, a, b)),
+            Fun({{A, Type()}, {B, Type()}, {a, A}, {b, A}}, eq(A, a, b)), env);
+    success(Fun({{A, Type()}, {B, Type()}, {a, A}, {b, _}}, eq(_, a, b)),
+            Fun({{A, Type()}, {B, Type()}, {a, A}, {b, A}}, eq(A, a, b)), env);
+    success(Fun({{A, Type()}, {B, Type()}, {a, B}, {b, _}}, eq(_, a, b)),
+            Fun({{A, Type()}, {B, Type()}, {a, B}, {b, B}}, eq(B, a, b)), env);
+    success(Fun({{A, Type()}, {B, Type()}, {a, B}, {b, _}, {C, Type()}}, eq(_, a, b)),
+            Fun({{A, Type()}, {B, Type()}, {a, B}, {b, B}, {C, Type()}}, eq(B, a, b)), env);
+    fails(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, _}, {C, Type()}}, eq(C, a, b)), env);
+    success(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, _}, {C, Type()}}, eq(B, a, b)),
+            Fun({{A, Type()}, {B, Type()}, {a, B}, {b, B}, {C, Type()}}, eq(B, a, b)), env);
 }
 
 
@@ -299,28 +299,28 @@ static void tst11() {
     env.add_var("a", Bool);
     env.add_var("b", Bool);
     env.add_var("c", Bool);
-    success(Fun({{H1, Eq(a,b)},{H2,Eq(b,c)}},
-                Trans(_,_,_,_,H1,H2)),
-            Fun({{H1, Eq(a,b)},{H2,Eq(b,c)}},
-                Trans(Bool,a,b,c,H1,H2)),
+    success(Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}},
+                Trans(_, _, _, _, H1, H2)),
+            Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}},
+                Trans(Bool, a, b, c, H1, H2)),
             env);
     expr H3 = Const("H3");
-    success(Fun({{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
-                EqTIntro(_, EqMP(_,_,Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1))), H3))),
-            Fun({{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
-                EqTIntro(c, EqMP(a,c,Symm(Bool,c,a,Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1))), H3))),
+    success(Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
+                EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3))),
+            Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
+                EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3))),
             env);
     frontend env2;
-    success(Fun({{a,Bool},{b,Bool},{c,Bool},{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
-                EqTIntro(_, EqMP(_,_,Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1))), H3))),
-            Fun({{a,Bool},{b,Bool},{c,Bool},{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
-                EqTIntro(c, EqMP(a,c,Symm(Bool,c,a,Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1))), H3))),
+    success(Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
+                EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3))),
+            Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
+                EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3))),
             env2);
     expr A = Const("A");
-    success(Fun({{A,Type()},{a,A},{b,A},{c,A},{H1, Eq(a,b)},{H2,Eq(b,c)}},
-                Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1)))),
-            Fun({{A,Type()},{a,A},{b,A},{c,A},{H1, Eq(a,b)},{H2,Eq(b,c)}},
-                Symm(A,c,a,Trans(A,c,b,a,Symm(A,b,c,H2),Symm(A,a,b,H1)))),
+    success(Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
+                Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1)))),
+            Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
+                Symm(A, c, a, Trans(A, c, b, a, Symm(A, b, c, H2), Symm(A, a, b, H1)))),
             env2);
 }
 
@@ -360,7 +360,7 @@ void tst14() {
     expr h  = Const("h");
     expr D  = Const("D");
     env.add_var("R", Type() >> Bool);
-    env.add_var("r", Pi({A, Type()},R(A)));
+    env.add_var("r", Pi({A, Type()}, R(A)));
     env.add_var("h", Pi({A, Type()}, R(A)) >> Bool);
     env.add_var("eq", Pi({A, Type(level()+1)}, A >> (A >> Bool)));
     success(Let({{f, Fun({A, Type()}, r(_))},
diff --git a/src/tests/frontends/lean/lean_frontend.cpp b/src/tests/frontends/lean/lean_frontend.cpp
index 7ea6730c99..744b57ebc3 100644
--- a/src/tests/frontends/lean/lean_frontend.cpp
+++ b/src/tests/frontends/lean/lean_frontend.cpp
@@ -159,7 +159,7 @@ static void tst10() {
     expr x = Const("xxxxxxxxxxxx");
     expr y = Const("y");
     expr z = Const("foo");
-    expr e = Let({{x, True}, {y, And({x,x,x,x,x,x,x,x})}, {z, And(x, y)}}, Or({x, x, x, x, x, x, x, x, x, z, z, z, z, z, z, z}));
+    expr e = Let({{x, True}, {y, And({x, x, x, x, x, x, x, x})}, {z, And(x, y)}}, Or({x, x, x, x, x, x, x, x, x, z, z, z, z, z, z, z}));
     std::cout << e << "\n";
     std::cout << fmt(e) << "\n";
 }
@@ -188,7 +188,7 @@ static void tst11() {
     } catch (exception & ex) {
         std::cout << "Expected error: " << ex.what() << std::endl;
     }
-    f.add_var(name{"h","explicit"}, Pi({A, Type()}, A >> (A >> A)));
+    f.add_var(name{"h", "explicit"}, Pi({A, Type()}, A >> (A >> A)));
     f.add_var("h", Pi({A, Type()}, A >> (A >> A)));
     try {
         f.mark_implicit_arguments("h", {true, false, false});
diff --git a/src/tests/interval/interval.cpp b/src/tests/interval/interval.cpp
index 0c39fd904b..995b7ee4c5 100644
--- a/src/tests/interval/interval.cpp
+++ b/src/tests/interval/interval.cpp
@@ -84,10 +84,10 @@ static void tst2() {
     lean_assert(power(qi(-3, -2), 2) == qi(4, 9));
     std::cout << power(qi(false, -3, -2, true), 2) << " --> " << qi(true, 4, 9, false) << "\n";
     lean_assert(power(qi(false, -3, -2, true), 2) == qi(true, 4, 9, false));
-    lean_assert(power(qi(-3,-1), 3) == qi(-27, -1));
+    lean_assert(power(qi(-3, -1), 3) == qi(-27, -1));
     lean_assert(power(qi(-3, 4), 3) == qi(-27, 64));
-    lean_assert(power(qi(),3) == qi());
-    lean_assert(power(qi(),2) == qi(false, 0)); // (-oo, oo)^2 == [0, oo)
+    lean_assert(power(qi(), 3) == qi());
+    lean_assert(power(qi(), 2) == qi(false, 0)); // (-oo, oo)^2 == [0, oo)
 }
 
 int main() {
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index c124aa37dc..3cfb9f8f76 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -224,8 +224,8 @@ void tst6() {
 void tst7() {
     expr f  = Const("f");
     expr v  = Var(0);
-    expr a1 = max_sharing(f(v,v));
-    expr a2 = max_sharing(f(v,v));
+    expr a1 = max_sharing(f(v, v));
+    expr a2 = max_sharing(f(v, v));
     lean_assert(!is_eqp(a1, a2));
     expr b  = max_sharing(f(a1, a2));
     lean_assert(is_eqp(arg(b, 1), arg(b, 2)));
@@ -315,7 +315,7 @@ void tst12() {
     expr a = Const("a");
     expr x = Var(0);
     expr t = Type();
-    expr F = mk_pi("y", t, mk_lambda("x", t, f(f(f(x,a),Const("10")),x)));
+    expr F = mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), x)));
     expr G = deep_copy(F);
     lean_assert(F == G);
     lean_assert(!is_eqp(F, G));
@@ -325,12 +325,12 @@ void tst12() {
 void tst13() {
     expr f  = Const("f");
     expr v  = Var(0);
-    expr a1 = max_sharing(f(v,v));
-    expr a2 = max_sharing(f(v,v));
+    expr a1 = max_sharing(f(v, v));
+    expr a2 = max_sharing(f(v, v));
     lean_assert(!is_eqp(a1, a2));
     lean_assert(a1 == a2);
     max_sharing_fn M;
-    lean_assert(is_eqp(M(f(v,v)), M(f(v,v))));
+    lean_assert(is_eqp(M(f(v, v)), M(f(v, v))));
     lean_assert(is_eqp(M(a1), M(a2)));
 }
 
diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp
index 59e6293a35..421a5c2b0a 100644
--- a/src/tests/kernel/normalizer.cpp
+++ b/src/tests/kernel/normalizer.cpp
@@ -157,9 +157,9 @@ static void tst2() {
     expr h = Const("h");
     expr x = Var(0);
     expr y = Var(1);
-    lean_assert(normalize(f(x,x), env, extend(context(), name("f"), t, f(a))) == f(f(a), f(a)));
+    lean_assert(normalize(f(x, x), env, extend(context(), name("f"), t, f(a))) == f(f(a), f(a)));
     context c1 = extend(extend(context(), name("f"), t, f(a)), name("h"), t, h(x));
-    expr F1 = normalize(f(x,f(x)), env, c1);
+    expr F1 = normalize(f(x, f(x)), env, c1);
     lean_assert(F1 == f(h(f(a)), f(h(f(a)))));
     std::cout << F1 << "\n";
     expr F2 = normalize(mk_lambda("x", t, f(x, f(y))), env, c1);
@@ -168,10 +168,10 @@ static void tst2() {
     expr F3 = normalize(mk_lambda("y", t, mk_lambda("x", t, f(x, f(y)))), env, c1);
     std::cout << F3 << "\n";
     lean_assert(F3 == mk_lambda("y", t, mk_lambda("x", t, f(x, f(y)))));
-    context c2 = extend(extend(context(), name("foo"), t, mk_lambda("x", t, f(x, a))), name("bla"), t, mk_lambda("z", t, h(x,y)));
+    context c2 = extend(extend(context(), name("foo"), t, mk_lambda("x", t, f(x, a))), name("bla"), t, mk_lambda("z", t, h(x, y)));
     expr F4 = normalize(mk_lambda("x", t, f(x, f(y))), env, c2);
     std::cout << F4 << "\n";
-    lean_assert(F4 == mk_lambda("x", t, f(x, f(mk_lambda("z", t, h(x,mk_lambda("x", t, f(x, a))))))));
+    lean_assert(F4 == mk_lambda("x", t, f(x, f(mk_lambda("z", t, h(x, mk_lambda("x", t, f(x, a))))))));
     context c3 = extend(context(), name("x"), t);
     expr f5 = mk_app(mk_lambda("f", t, mk_lambda("z", t, Var(1))), mk_lambda("y", t, Var(1)));
     expr F5 = normalize(f5, env, c3);
@@ -180,7 +180,7 @@ static void tst2() {
     lean_assert(F5 == mk_lambda("z", t, mk_lambda("y", t, Var(2))));
     context c4 = extend(extend(context(), name("x"), t), name("x2"), t);
     expr F6 = normalize(mk_app(mk_lambda("f", t, mk_lambda("z1", t, mk_lambda("z2", t, mk_app(Var(2), Const("a"))))),
-                            mk_lambda("y", t, mk_app(Var(1), Var(2), Var(0)))), env, c4);
+                               mk_lambda("y", t, mk_app(Var(1), Var(2), Var(0)))), env, c4);
     std::cout << F6 << "\n";
     lean_assert(F6 == mk_lambda("z1", t, mk_lambda("z2", t, mk_app(Var(2), Var(3), Const("a")))));
 }
diff --git a/src/tests/kernel/replace.cpp b/src/tests/kernel/replace.cpp
index 294d1bb378..c137cea580 100644
--- a/src/tests/kernel/replace.cpp
+++ b/src/tests/kernel/replace.cpp
@@ -80,17 +80,17 @@ static void tst3() {
         }
     };
     replace_fn<decltype(proc), tracer> replacer(proc, tracer(trace));
-    expr t = Fun({{x, A}, {y, A}}, f(x, f(f(f(x,x), f(y, d)), f(d, d))));
+    expr t = Fun({{x, A}, {y, A}}, f(x, f(f(f(x, x), f(y, d)), f(d, d))));
     expr b = abst_body(t);
     expr r = replacer(b);
     std::cout << r << "\n";
-    lean_assert(r == Fun({y, A}, f(c, f(f(f(c,c), f(y, d)), f(d, d)))));
+    lean_assert(r == Fun({y, A}, f(c, f(f(f(c, c), f(y, d)), f(d, d)))));
     for (auto p : trace) {
         std::cout << p.first << " --> " << p.second << "\n";
     }
     lean_assert(trace[c] == Var(1));
     std::cout << arg(arg(abst_body(r), 2), 2) << "\n";
-    lean_assert(arg(arg(abst_body(r), 2), 2) == f(d,d));
+    lean_assert(arg(arg(abst_body(r), 2), 2) == f(d, d));
     lean_assert(trace.find(arg(arg(abst_body(r), 2), 2)) == trace.end());
     lean_assert(trace.find(abst_body(r)) != trace.end());
     lean_assert(trace.find(arg(abst_body(r), 2)) != trace.end());
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index 532cc17d34..9535960dba 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -194,18 +194,18 @@ static void tst11() {
     unsigned n = 1000;
     expr f = Const("f");
     expr a = Const("a");
-    expr t1 = f(a,a);
+    expr t1 = f(a, a);
     expr b = Const("a");
-    expr t2 = f(a,a);
-    expr t3 = f(b,b);
+    expr t2 = f(a, a);
+    expr t3 = f(b, b);
     for (unsigned i = 0; i < n; i++) {
-        t1 = f(t1,t1);
+        t1 = f(t1, t1);
         t2 = mk_let("x", expr(), t2, f(Var(0), Var(0)));
-        t3 = f(t3,t3);
+        t3 = f(t3, t3);
     }
     lean_assert(t1 != t2);
-    env.add_theorem("eqs1", Eq(t1,t2), Refl(Int, t1));
-    env.add_theorem("eqs2", Eq(t1,t3), Refl(Int, t1));
+    env.add_theorem("eqs1", Eq(t1, t2), Refl(Int, t1));
+    env.add_theorem("eqs2", Eq(t1, t3), Refl(Int, t1));
 }
 
 static expr mk_big(unsigned depth) {
@@ -244,7 +244,7 @@ static void tst13() {
     env.add_var("f", Type() >> Type());
     expr f = Const("f");
     std::cout << infer_type(f(Bool), env) << "\n";
-    std::cout << infer_type(f(Eq(True,False)), env) << "\n";
+    std::cout << infer_type(f(Eq(True, False)), env) << "\n";
 }
 
 int main() {
diff --git a/src/tests/library/light_checker.cpp b/src/tests/library/light_checker.cpp
index 08af890084..8ba892e8a5 100644
--- a/src/tests/library/light_checker.cpp
+++ b/src/tests/library/light_checker.cpp
@@ -24,10 +24,10 @@ static void tst1() {
     expr b = Const("b");
     expr A = Const("A");
     env.add_var("f", Int >> (Int >> Int));
-    lean_assert(type_of(f(a,a)) == Int);
+    lean_assert(type_of(f(a, a)) == Int);
     lean_assert(type_of(f(a)) == Int >> Int);
     lean_assert(type_of(And(a, f(a))) == Bool);
-    lean_assert(type_of(Fun({a, Int}, iAdd(a,iVal(1)))) == Int >> Int);
+    lean_assert(type_of(Fun({a, Int}, iAdd(a, iVal(1)))) == Int >> Int);
     lean_assert(type_of(Let({a, iVal(10)}, iAdd(a, b))) == Int);
     lean_assert(type_of(Type()) == Type(level() + 1));
     lean_assert(type_of(Bool) == Type());
diff --git a/src/tests/library/metavar.cpp b/src/tests/library/metavar.cpp
index 4e6198d379..51a74402b1 100644
--- a/src/tests/library/metavar.cpp
+++ b/src/tests/library/metavar.cpp
@@ -51,7 +51,7 @@ static void tst3() {
     expr r = instantiate_free_var_mmv(t, 0, a);
     r = instantiate_metavar(r, 1, g(Var(0), Var(1)));
     std::cout << r << std::endl;
-    lean_assert(r == f(g(a,Var(0)), a, Var(1)));
+    lean_assert(r == f(g(a, Var(0)), a, Var(1)));
 }
 
 static void tst4() {
@@ -66,7 +66,7 @@ static void tst4() {
     std::cout << r << std::endl;
     r = instantiate_metavar(r, 1, g(Var(0), Var(1)));
     std::cout << r << std::endl;
-    lean_assert(r == f(g(a,Var(2)), Var(2), Var(3)));
+    lean_assert(r == f(g(a, Var(2)), Var(2), Var(3)));
 }
 
 static void tst5() {
@@ -98,7 +98,7 @@ static void tst6() {
     expr a  = Const("a");
     expr x  = Const("x");
     expr m1 = mk_metavar(1);
-    expr t  = mk_app(Fun({x,N}, m1), a);
+    expr t  = mk_app(Fun({x, N}, m1), a);
     expr s1 = instantiate_metavar(head_reduce_mmv(t, env), 1, Var(0));
     expr s2 = head_reduce_mmv(instantiate_metavar(t, 1, Var(0)), env);
     std::cout << instantiate_metavar(t, 1, Var(0)) << "\n";
diff --git a/src/tests/util/format.cpp b/src/tests/util/format.cpp
index 53f51373a8..19774af4a9 100644
--- a/src/tests/util/format.cpp
+++ b/src/tests/util/format.cpp
@@ -107,7 +107,7 @@ static void tst4() {
     s << pp(sexpr()) << " ";
     s << pp(sexpr("test")) << " ";
     sexpr s1(mpz(100));
-    sexpr s2(mpq(1,2));
+    sexpr s2(mpq(1, 2));
     sexpr s3{s1, s2};
     s << pp(s3);
     std::cout << s.str() << "\n";
diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp
index 272ee4f2bf..225df70322 100644
--- a/src/tests/util/name.cpp
+++ b/src/tests/util/name.cpp
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <sstream>
 #include "util/test.h"
 #include "util/name.h"
-using namespace lean;
+ using namespace lean;
 
 static void tst1() {
     name n("foo");
@@ -27,7 +27,7 @@ static void tst1() {
     lean_assert(name(name(), "foo") == name("foo"));
 
     lean_assert(name(n, 1) < name(n, 2));
-    std::cout << "cmp(" << name(n, 1) << ", " << name(n, 2) << ") = " << cmp(name(n,1), name(n, 2)) << "\n";
+    std::cout << "cmp(" << name(n, 1) << ", " << name(n, 2) << ") = " << cmp(name(n, 1), name(n, 2)) << "\n";
     lean_assert(!(name(n, 1) >= name(n, 2)));
     lean_assert(name(n, 1) < name(name(n, 1), 1));
     lean_assert(n < name(n, 1));
diff --git a/src/tests/util/numerics/mpbq.cpp b/src/tests/util/numerics/mpbq.cpp
index 6b5c9ad986..3e4d8cfe38 100644
--- a/src/tests/util/numerics/mpbq.cpp
+++ b/src/tests/util/numerics/mpbq.cpp
@@ -12,26 +12,26 @@ Author: Leonardo de Moura
 using namespace lean;
 
 static void tst1() {
-    mpbq a(1,1);
+    mpbq a(1, 1);
     std::cout << a << "\n";
-    lean_assert(a == mpq(1,2));
-    std::cout << mpbq(mpq(1,3)) << "\n";
-    lean_assert(!set(a, mpq(1,3)));
-    lean_assert(a == mpbq(1,2));
+    lean_assert(a == mpq(1, 2));
+    std::cout << mpbq(mpq(1, 3)) << "\n";
+    lean_assert(!set(a, mpq(1, 3)));
+    lean_assert(a == mpbq(1, 2));
     mpq b;
     b = a;
-    lean_assert(b == mpq(1,4));
+    lean_assert(b == mpq(1, 4));
     lean_assert(inv(b) == 4);
-    lean_assert(a/2 == mpbq(1,3));
+    lean_assert(a/2 == mpbq(1, 3));
     lean_assert(a/1 == a);
-    lean_assert(a/8 == mpbq(1,5));
-    lean_assert((3*a)/8 == mpbq(3,5));
+    lean_assert(a/8 == mpbq(1, 5));
+    lean_assert((3*a)/8 == mpbq(3, 5));
     mpbq l(0), u(1);
-    mpq v(1,3);
+    mpq v(1, 3);
     while (true) {
         lean_assert(l < v);
         lean_assert(v < u);
-        std::cout << mpbq::decimal(l,20) << " " << v << " " << mpbq::decimal(u, 20) << "\n";
+        std::cout << mpbq::decimal(l, 20) << " " << v << " " << mpbq::decimal(u, 20) << "\n";
         if (lt_1div2k((u - l)/2, 50))
             break;
         refine_lower(v, l, u);
@@ -44,31 +44,31 @@ static void tst2() {
     std::ostringstream out;
     out << num;
     lean_assert(out.str() == "2");
-    mpbq a(-1,2);
+    mpbq a(-1, 2);
     std::ostringstream out2;
     display_decimal(out2, a, 10);
     lean_assert(out2.str() == "-0.25");
     lean_assert(lt_1div2k(a, 8));
     mul2(a);
-    lean_assert(a == mpbq(-1,1));
+    lean_assert(a == mpbq(-1, 1));
     mul2k(a, 3);
     lean_assert(a == mpbq(-4));
     mul2k(a, 0);
     lean_assert(a == mpbq(-4));
     mul2k(a, 2);
     lean_assert(a == mpbq(-16));
-    lean_assert(cmp(mpbq(1,2), mpbq(1,4)) == 1);
-    lean_assert(cmp(mpbq(1,2), mpbq(1,2)) == 0);
-    lean_assert(cmp(mpbq(1,2), mpbq(3,2)) == -1);
-    lean_assert(cmp(mpbq(3,2), mpbq(3,4)) == 1);
-    lean_assert(cmp(mpbq(15,2), mpbq(3,1)) == 1);
-    lean_assert(cmp(mpbq(7,1), mpz(3)) == 1);
-    lean_assert(cmp(mpbq(3,0), mpz(3)) == 0);
-    lean_assert(cmp(mpbq(2,0), mpz(3)) == -1);
-    lean_assert(cmp(mpbq(7,4), mpz(10)) == -1);
-    lean_assert(mpbq(0,1) == mpz(0));
-    set(a, mpq(1,4));
-    lean_assert(cmp(a, mpbq(1,2)) == 0);
+    lean_assert(cmp(mpbq(1, 2), mpbq(1, 4)) == 1);
+    lean_assert(cmp(mpbq(1, 2), mpbq(1, 2)) == 0);
+    lean_assert(cmp(mpbq(1, 2), mpbq(3, 2)) == -1);
+    lean_assert(cmp(mpbq(3, 2), mpbq(3, 4)) == 1);
+    lean_assert(cmp(mpbq(15, 2), mpbq(3, 1)) == 1);
+    lean_assert(cmp(mpbq(7, 1), mpz(3)) == 1);
+    lean_assert(cmp(mpbq(3, 0), mpz(3)) == 0);
+    lean_assert(cmp(mpbq(2, 0), mpz(3)) == -1);
+    lean_assert(cmp(mpbq(7, 4), mpz(10)) == -1);
+    lean_assert(mpbq(0, 1) == mpz(0));
+    set(a, mpq(1, 4));
+    lean_assert(cmp(a, mpbq(1, 2)) == 0);
     set(a, mpq(0));
     lean_assert(a.is_zero());
     a += 3u;
@@ -76,15 +76,15 @@ static void tst2() {
     a += -2;
     lean_assert(a == 1);
     div2k(a, 2);
-    lean_assert(a == mpq(1,4));
+    lean_assert(a == mpq(1, 4));
     a += 3u;
-    lean_assert(a == mpq(13,4));
+    lean_assert(a == mpq(13, 4));
     a += -2;
-    lean_assert(a == mpq(5,4));
+    lean_assert(a == mpq(5, 4));
     a -= 1u;
-    lean_assert(a == mpq(1,4));
+    lean_assert(a == mpq(1, 4));
     a -= -2;
-    lean_assert(a == mpq(9,4));
+    lean_assert(a == mpq(9, 4));
 }
 
 int main() {
diff --git a/src/tests/util/numerics/mpq.cpp b/src/tests/util/numerics/mpq.cpp
index 6099cd8a8c..c862435f7a 100644
--- a/src/tests/util/numerics/mpq.cpp
+++ b/src/tests/util/numerics/mpq.cpp
@@ -17,9 +17,9 @@ static void tst0() {
 }
 
 static void tst1() {
-    mpq a(2,3), b(4,3);
+    mpq a(2, 3), b(4, 3);
     b = a / b;
-    lean_assert(b == mpq(1,2));
+    lean_assert(b == mpq(1, 2));
     a = mpq(2);
     a.inv();
     lean_assert(a == b);
@@ -30,7 +30,7 @@ static void tst1() {
 }
 
 static void tst2() {
-    mpq a(2,3);
+    mpq a(2, 3);
     lean_assert(floor(a) == 0);
     lean_assert(ceil(a) == 1);
     mpq b(-2, 3);
@@ -58,35 +58,35 @@ static void tst3() {
 }
 
 static void tst4() {
-    mpq a(8,6);
-    lean_assert(a == mpq(4,3));
-    lean_assert(mpq(1,2)+mpq(1,2) == mpq(1));
+    mpq a(8, 6);
+    lean_assert(a == mpq(4, 3));
+    lean_assert(mpq(1, 2)+mpq(1, 2) == mpq(1));
     lean_assert(mpq("1/2") < mpq("2/3"));
-    lean_assert(mpq(-1,2).is_neg());
-    lean_assert(mpq(-1,2).is_nonpos());
-    lean_assert(!mpq(-1,2).is_zero());
-    lean_assert(mpq(1,2) > mpq());
+    lean_assert(mpq(-1, 2).is_neg());
+    lean_assert(mpq(-1, 2).is_nonpos());
+    lean_assert(!mpq(-1, 2).is_zero());
+    lean_assert(mpq(1, 2) > mpq());
     lean_assert(mpq().is_zero());
-    lean_assert(mpq(2,3) + mpq(4,3) == mpq(2));
-    lean_assert(mpq(1,2) >= mpq(1,3));
-    lean_assert(mpq(3,4).get_denominator() == 4);
-    lean_assert(mpq(3,4).get_numerator() == 3);
-    lean_assert(mpq(1,2) / mpq(5,4) == mpq(2,5));
-    lean_assert(mpq(1,2) - mpq(2,3) == mpq(-1,6));
-    lean_assert(mpq(3,4) * mpq(2,3) == mpq(1,2));
+    lean_assert(mpq(2, 3) + mpq(4, 3) == mpq(2));
+    lean_assert(mpq(1, 2) >= mpq(1, 3));
+    lean_assert(mpq(3, 4).get_denominator() == 4);
+    lean_assert(mpq(3, 4).get_numerator() == 3);
+    lean_assert(mpq(1, 2) / mpq(5, 4) == mpq(2, 5));
+    lean_assert(mpq(1, 2) - mpq(2, 3) == mpq(-1, 6));
+    lean_assert(mpq(3, 4) * mpq(2, 3) == mpq(1, 2));
     a *= 3;
     lean_assert(a == 4);
     a /= 2;
     lean_assert(a == 2);
     lean_assert(a.is_integer());
     a /= 5;
-    lean_assert(a == mpq(2,5));
+    lean_assert(a == mpq(2, 5));
     lean_assert(!a.is_integer());
-    mpq b(3,7);
+    mpq b(3, 7);
     a *= b;
-    lean_assert(a == mpq(6,35));
+    lean_assert(a == mpq(6, 35));
     a /= b;
-    lean_assert(a == mpq(2,5));
+    lean_assert(a == mpq(2, 5));
     mpz c(5);
     a *= c;
     lean_assert(a == 2);
@@ -95,7 +95,7 @@ static void tst4() {
     a -= c;
     lean_assert(a == 2);
     a /= c;
-    lean_assert(a == mpq(2,5));
+    lean_assert(a == mpq(2, 5));
 }
 
 static void tst5() {
@@ -123,7 +123,7 @@ static void tst5() {
     lean_assert(1u >= a);
     lean_assert(2u > a);
     a = "1/3";
-    lean_assert(a == mpq(1,3));
+    lean_assert(a == mpq(1, 3));
     a = 2.0;
     lean_assert(a == mpq(2));
     a = mpz(10);
@@ -147,30 +147,30 @@ static void tst6() {
     lean_assert(v1 == 1);
     v1.ceil();
     lean_assert(v1 == 1);
-    v1 = mpq(1,2);
+    v1 = mpq(1, 2);
     v1.floor();
     lean_assert(v1 == 0);
-    v1 = mpq(1,2);
+    v1 = mpq(1, 2);
     v1.ceil();
     lean_assert(v1 == 1);
     v1 -= 2u;
     lean_assert(v1 == -1);
-    v1 = mpq(-1,2);
+    v1 = mpq(-1, 2);
     v1.floor();
     lean_assert(v1 == -1);
-    v1 = mpq(-1,2);
+    v1 = mpq(-1, 2);
     v1.ceil();
     lean_assert(v1 == 0);
-    check_dec(mpq(-1,2), "-0.5");
-    check_dec(mpq(1,3),  "0.33333?", 5);
+    check_dec(mpq(-1, 2), "-0.5");
+    check_dec(mpq(1, 3),  "0.33333?", 5);
     check_dec(mpq(3),    "3");
-    check_dec(mpq(-2,1), "-2");
-    check_dec(mpq(-1,3),  "-0.33333?", 5);
-    check_dec(mpq(-1,7),  "-0.14285?", 5);
+    check_dec(mpq(-2, 1), "-2");
+    check_dec(mpq(-1, 3),  "-0.33333?", 5);
+    check_dec(mpq(-1, 7),  "-0.14285?", 5);
 
-    lean_assert(cmp(mpq(1,2), mpz(1)) < 0);
-    lean_assert(cmp(mpq(3,2), mpz(1)) > 0);
-    lean_assert(cmp(mpq(-3,2), mpz(-1)) < 0);
+    lean_assert(cmp(mpq(1, 2), mpz(1)) < 0);
+    lean_assert(cmp(mpq(3, 2), mpz(1)) > 0);
+    lean_assert(cmp(mpq(-3, 2), mpz(-1)) < 0);
 }
 
 int main() {
diff --git a/src/tests/util/sexpr.cpp b/src/tests/util/sexpr.cpp
index 05b7bfe4ba..20a5f5362f 100644
--- a/src/tests/util/sexpr.cpp
+++ b/src/tests/util/sexpr.cpp
@@ -49,9 +49,9 @@ static void tst1() {
     lean_assert(is_list(sexpr{10.2}));
     lean_assert(len(sexpr{10.2}) == 1);
     // list of pairs
-    std::cout << sexpr{ sexpr(1,2), sexpr(2,3), sexpr(0,1) } << "\n";
+    std::cout << sexpr{ sexpr(1, 2), sexpr(2, 3), sexpr(0, 1) } << "\n";
     // list of lists
-    std::cout << sexpr{ sexpr{1,2}, sexpr{2,3}, sexpr{0,1} } << "\n";
+    std::cout << sexpr{ sexpr{1, 2}, sexpr{2, 3}, sexpr{0, 1} } << "\n";
     lean_assert(reverse(sexpr{1, 2, 3}) == (sexpr{3, 2, 1}));
     sexpr l = map(sexpr{1, 2, 3},
                   [](sexpr e) {
@@ -67,11 +67,11 @@ static void tst1() {
     lean_assert(member(3, sexpr{10, 2, 3, 1}));
     lean_assert(!member(3, nil()));
     lean_assert(!member(3, sexpr{10, 2, 1}));
-    lean_assert(append(sexpr{1,2}, sexpr{3,4}) == (sexpr{1,2,3,4}));
+    lean_assert(append(sexpr{1, 2}, sexpr{3, 4}) == (sexpr{1, 2, 3, 4}));
     lean_assert(append(l, nil()) == l);
     lean_assert(append(nil(), l) == l);
-    lean_assert(contains(sexpr{10,20,-2,0,10}, [](sexpr e) { return to_int(e) < 0; }));
-    lean_assert(!contains(sexpr{10,20,-2,0,10}, [](sexpr e) { return to_int(e) < -10; }));
+    lean_assert(contains(sexpr{10, 20, -2, 0, 10}, [](sexpr e) { return to_int(e) < 0; }));
+    lean_assert(!contains(sexpr{10, 20, -2, 0, 10}, [](sexpr e) { return to_int(e) < -10; }));
     lean_assert(is_eqp(s1, s1));
     sexpr s3 = s1;
     lean_assert(is_eqp(s1, s3));
@@ -101,12 +101,12 @@ static void tst2() {
     lean_assert(a == sexpr(name(name("foo"), 1)));
     lean_assert(a == name(name("foo"), 1));
     lean_assert(name(name("foo"), 1) == a);
-    a = mpq(1,3);
-    lean_assert(a == sexpr(mpq(1,3)));
-    lean_assert(a == mpq(1,3));
+    a = mpq(1, 3);
+    lean_assert(a == sexpr(mpq(1, 3)));
+    lean_assert(a == mpq(1, 3));
     lean_assert(mpq(1, 3) == a);
     lean_assert(mpq(2, 3) != a);
-    a = power(mpz(2),100);
+    a = power(mpz(2), 100);
     lean_assert(a == sexpr(power(mpz(2), 100)));
     lean_assert(a == power(mpz(2), 100));
     lean_assert(power(mpz(2), 100) == a);
@@ -142,14 +142,14 @@ static void tst4() {
 }
 
 static void tst5() {
-    lean_assert(foldl(sexpr{1,2,3,4,5,6,7,8,9},
+    lean_assert(foldl(sexpr{1, 2, 3, 4, 5, 6, 7, 8, 9},
                       0,
                       [](int result, sexpr const & s) {
                           return result * 10 + to_int(s);
                       })
                 == 123456789);
 
-    lean_assert(foldr(sexpr{1,2,3,4,5,6,7,8,9},
+    lean_assert(foldr(sexpr{1, 2, 3, 4, 5, 6, 7, 8, 9},
                       0,
                       [](sexpr const & s, int result) {
                           return result * 10 + to_int(s);
@@ -165,9 +165,9 @@ static void tst6() {
 }
 
 static void tst7() {
-    sexpr s = sexpr{ sexpr(1,2), sexpr(2,3), sexpr(0,1) };
+    sexpr s = sexpr{ sexpr(1, 2), sexpr(2, 3), sexpr(0, 1) };
     std::cout << pp(sexpr{s, s, s, s, s}) << "\n";
-    std::cout << pp(sexpr{sexpr(name{"test","name"}), sexpr(10), sexpr(10.20)}) << "\n";
+    std::cout << pp(sexpr{sexpr(name{"test", "name"}), sexpr(10), sexpr(10.20)}) << "\n";
     format f = highlight(pp(sexpr{s, s, s, s, s}));
     std::cout << f << "\n";
     std::cout << mk_pair(f, options({"pp", "width"}, 1000)) << "\n";
@@ -194,10 +194,10 @@ static void tst8() {
     lean_assert(cmp(sexpr(name("aaa")), sexpr(name("bbb"))) < 0);
     lean_assert(cmp(sexpr(mpz(10)), sexpr(mpz(10))) == 0);
     lean_assert(cmp(sexpr(mpz(20)), sexpr(mpz(10))) > 0);
-    lean_assert(cmp(sexpr(mpq(1,2)), sexpr(mpq(1,2))) == 0);
-    lean_assert(cmp(sexpr(mpq(1,3)), sexpr(mpq(1,2))) < 0);
+    lean_assert(cmp(sexpr(mpq(1, 2)), sexpr(mpq(1, 2))) == 0);
+    lean_assert(cmp(sexpr(mpq(1, 3)), sexpr(mpq(1, 2))) < 0);
     std::ostringstream s;
-    s << sexpr() << " " << sexpr(mpq(1,2));
+    s << sexpr() << " " << sexpr(mpq(1, 2));
     std::cout << s.str() << "\n";
     lean_assert(s.str() == "nil 1/2");
 }
diff --git a/src/util/hash.cpp b/src/util/hash.cpp
index c4a8f6361e..e2e8af337b 100644
--- a/src/util/hash.cpp
+++ b/src/util/hash.cpp
@@ -33,7 +33,7 @@ unsigned hash_str(unsigned length, char const * str, unsigned init_value) {
         a += reinterpret_cast<unsigned const *>(str)[0];
         b += reinterpret_cast<unsigned const *>(str)[1];
         c += reinterpret_cast<unsigned const *>(str)[2];
-        mix(a,b,c);
+        mix(a, b, c);
         str += 12; len -= 12;
     }
 
@@ -55,7 +55,7 @@ unsigned hash_str(unsigned length, char const * str, unsigned init_value) {
     case 1 :  a+=str[0];
         /* case 0: nothing left to add */
     }
-    mix(a,b,c);
+    mix(a, b, c);
     /*-------------------------------------------- report the result */
     return c;
 }
diff --git a/src/util/numerics/mpbq.h b/src/util/numerics/mpbq.h
index 70926662e2..09b6ae8261 100644
--- a/src/util/numerics/mpbq.h
+++ b/src/util/numerics/mpbq.h
@@ -124,15 +124,15 @@ public:
     friend bool operator==(unsigned int a, mpbq const & b) { return operator==(b, a); }
     friend bool operator==(int a, mpbq const & b) { return operator==(b, a); }
 
-    friend bool operator!=(mpbq const & a, mpbq const & b) { return !operator==(a,b); }
-    friend bool operator!=(mpbq const & a, mpz const & b) { return !operator==(a,b); }
-    friend bool operator!=(mpbq const & a, mpq const & b) { return !operator==(a,b); }
-    friend bool operator!=(mpbq const & a, unsigned int b) { return !operator==(a,b); }
-    friend bool operator!=(mpbq const & a, int b) { return !operator==(a,b); }
-    friend bool operator!=(mpz const & a, mpbq const & b) { return !operator==(a,b); }
-    friend bool operator!=(mpq const & a, mpbq const & b) { return !operator==(a,b); }
-    friend bool operator!=(unsigned int a, mpbq const & b) { return !operator==(a,b); }
-    friend bool operator!=(int a, mpbq const & b) { return !operator==(a,b); }
+    friend bool operator!=(mpbq const & a, mpbq const & b) { return !operator==(a, b); }
+    friend bool operator!=(mpbq const & a, mpz const & b) { return !operator==(a, b); }
+    friend bool operator!=(mpbq const & a, mpq const & b) { return !operator==(a, b); }
+    friend bool operator!=(mpbq const & a, unsigned int b) { return !operator==(a, b); }
+    friend bool operator!=(mpbq const & a, int b) { return !operator==(a, b); }
+    friend bool operator!=(mpz const & a, mpbq const & b) { return !operator==(a, b); }
+    friend bool operator!=(mpq const & a, mpbq const & b) { return !operator==(a, b); }
+    friend bool operator!=(unsigned int a, mpbq const & b) { return !operator==(a, b); }
+    friend bool operator!=(int a, mpbq const & b) { return !operator==(a, b); }
 
     mpbq & operator+=(mpbq const & a);
     mpbq & operator+=(unsigned a);
diff --git a/src/util/numerics/mpfp.h b/src/util/numerics/mpfp.h
index e3b2a78d77..6da4a7d9a2 100644
--- a/src/util/numerics/mpfp.h
+++ b/src/util/numerics/mpfp.h
@@ -299,7 +299,7 @@ public:
     friend bool operator==(mpfp const & a, mpq_t const & b          ) { return cmp(a, b) == 0; }
     friend bool operator==(mpfp const & a, mpf_t const & b          ) { return cmp(a, b) == 0; }
 
-    friend bool operator!=(mpfp const & a, mpfp const & b) { return !operator==(a,b); }
+    friend bool operator!=(mpfp const & a, mpfp const & b) { return !operator==(a, b); }
     friend bool operator!=(unsigned long int const a, mpfp const & b) { return cmp(b, a) != 0; }
     friend bool operator!=(long int const a         , mpfp const & b) { return cmp(b, a) != 0; }
     friend bool operator!=(double const a           , mpfp const & b) { return cmp(b, a) != 0; }
diff --git a/src/util/numerics/mpq.h b/src/util/numerics/mpq.h
index 7b5284ac94..bf3abdfb3c 100644
--- a/src/util/numerics/mpq.h
+++ b/src/util/numerics/mpq.h
@@ -121,13 +121,13 @@ public:
     friend bool operator==(unsigned int a, mpq const & b) { return operator==(b, a); }
     friend bool operator==(int a, mpq const & b) { return operator==(b, a); }
 
-    friend bool operator!=(mpq const & a, mpq const & b) { return !operator==(a,b); }
-    friend bool operator!=(mpq const & a, mpz const & b) { return !operator==(a,b); }
-    friend bool operator!=(mpq const & a, unsigned int b) { return !operator==(a,b); }
-    friend bool operator!=(mpq const & a, int b) { return !operator==(a,b); }
-    friend bool operator!=(mpz const & a, mpq const & b) { return !operator==(a,b); }
-    friend bool operator!=(unsigned int a, mpq const & b) { return !operator==(a,b); }
-    friend bool operator!=(int a, mpq const & b) { return !operator==(a,b); }
+    friend bool operator!=(mpq const & a, mpq const & b) { return !operator==(a, b); }
+    friend bool operator!=(mpq const & a, mpz const & b) { return !operator==(a, b); }
+    friend bool operator!=(mpq const & a, unsigned int b) { return !operator==(a, b); }
+    friend bool operator!=(mpq const & a, int b) { return !operator==(a, b); }
+    friend bool operator!=(mpz const & a, mpq const & b) { return !operator==(a, b); }
+    friend bool operator!=(unsigned int a, mpq const & b) { return !operator==(a, b); }
+    friend bool operator!=(int a, mpq const & b) { return !operator==(a, b); }
 
     mpq & operator+=(mpq const & o) { mpq_add(m_val, m_val, o.m_val); return *this; }
     mpq & operator+=(mpz const & o) { mpz_addmul(mpq_numref(m_val), mpq_denref(m_val), o.m_val); mpq_canonicalize(m_val); return *this; }
diff --git a/src/util/numerics/xnumeral.h b/src/util/numerics/xnumeral.h
index e563146fb1..a03f20503c 100644
--- a/src/util/numerics/xnumeral.h
+++ b/src/util/numerics/xnumeral.h
@@ -186,7 +186,7 @@ void power(T & a, xnumeral_kind & ak, unsigned n) {
 }
 
 /**
-   \brief Return true if (a,ak) == (b,bk).
+   \brief Return true if (a, ak) == (b, bk).
 */
 template<typename T>
 bool eq(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) {
diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h
index f7f47e6a12..0a353e09c4 100644
--- a/src/util/sexpr/options.h
+++ b/src/util/sexpr/options.h
@@ -70,8 +70,8 @@ struct mk_option_declaration {
 #define LEAN_MAKE_OPTION_NAME_CORE(LINE) LEAN_OPTION_ ## LINE
 #define LEAN_MAKE_OPTION_NAME(LINE) LEAN_MAKE_OPTION_NAME_CORE(LINE)
 #define LEAN_OPTION_UNIQUE_NAME LEAN_MAKE_OPTION_NAME(__LINE__)
-#define RegisterOption(N,K,D,DESC) static ::lean::mk_option_declaration LEAN_OPTION_UNIQUE_NAME(N,K,D,DESC)
-#define RegisterOptionCore(N,K,D,DESC) RegisterOption(N,K,#D,DESC)
-#define RegisterBoolOption(N,D,DESC) RegisterOptionCore(N, BoolOption, D, DESC);
-#define RegisterUnsignedOption(N,D,DESC) RegisterOptionCore(N, UnsignedOption, D, DESC);
+#define RegisterOption(N, K, D, DESC) static ::lean::mk_option_declaration LEAN_OPTION_UNIQUE_NAME(N, K, D, DESC)
+#define RegisterOptionCore(N, K, D, DESC) RegisterOption(N, K, #D, DESC)
+#define RegisterBoolOption(N, D, DESC) RegisterOptionCore(N, BoolOption, D, DESC);
+#define RegisterUnsignedOption(N, D, DESC) RegisterOptionCore(N, UnsignedOption, D, DESC);
 }