diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h
index 7b4c9de22..b7ae43c56 100644
--- a/src/interval/interval_def.h
+++ b/src/interval/interval_def.h
@@ -146,8 +146,7 @@ void interval<T>::neg() {
         if (is_upper_inf()) {
             // (-oo, oo) case
             // do nothing
-        }
-        else {
+        } else {
             // (-oo, a| --> |-a, oo)
             swap(m_lower, m_upper);
             neg(m_lower);
@@ -158,8 +157,7 @@ void interval<T>::neg() {
             m_upper_inf  = true;
             m_upper_open = true;
         }
-    }
-    else {
+    } else {
         if (is_upper_inf()) {
             // |a, oo) --> (-oo, -a|
             swap(m_upper, m_lower);
@@ -170,8 +168,7 @@ void interval<T>::neg() {
             reset(m_lower);
             m_lower_inf  = true;
             m_lower_open = true;
-        }
-        else {
+        } else {
             // |a, b| --> |-b, -a|
             swap(m_lower, m_upper);
             neg(m_lower);
@@ -270,8 +267,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
             mul(new_l_val, new_l_kind, b, b_k, d, d_k);
             round_to_plus_inf();
             mul(new_u_val, new_u_kind, a, a_k, c, c_k);
-        }
-        else if (i2.is_M()) {
+        } else if (i2.is_M()) {
             // a <= x <= b <= 0,  y <= d, d > 0 --> a*d <= x*y (uses the fact that b is not positive)
             // a <= x <= b <= 0,  c <= y, c < 0 --> x*y <= a*c (uses the fact that b is not positive)
             set_is_lower_open(a_o || d_o);
@@ -281,8 +277,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
             mul(new_l_val, new_l_kind, a, a_k, d, d_k);
             round_to_plus_inf();
             mul(new_u_val, new_u_kind, a, a_k, c, c_k);
-        }
-        else {
+        } else {
             // a <= x <= b <= 0, 0 <= c <= y <= d --> a*d <= x*y (uses the fact that x is neg (b is not positive) or y is pos (c is not negative))
             // x <= b <= 0,  0 <= c <= y --> x*y <= b*c
             lean_assert(i2.is_P());
@@ -296,8 +291,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
             round_to_plus_inf();
             mul(new_u_val, new_u_kind, b, b_k, c, c_k);
         }
-    }
-    else if (i1.is_M()) {
+    } else if (i1.is_M()) {
         if (i2.is_N()) {
             // b > 0, x <= b,  c <= y <= d <= 0 --> b*c <= x*y (uses the fact that d is not positive)
             // a < 0, a <= x,  c <= y <= d <= 0 --> x*y <= a*c (uses the fact that d is not positive)
@@ -308,8 +302,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
             mul(new_l_val, new_l_kind, b, b_k, c, c_k);
             round_to_plus_inf();
             mul(new_u_val, new_u_kind, a, a_k, c, c_k);
-        }
-        else if (i2.is_M()) {
+        } else if (i2.is_M()) {
             static thread_local T ad; xnumeral_kind ad_k;
             static thread_local T bc; xnumeral_kind bc_k;
             static thread_local T ac; xnumeral_kind ac_k;
@@ -331,8 +324,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
                 swap(new_l_val, ad);
                 new_l_kind = ad_k;
                 set_is_lower_open(ad_o);
-            }
-            else {
+            } else {
                 swap(new_l_val, bc);
                 new_l_kind = bc_k;
                 set_is_lower_open(bc_o);
@@ -343,14 +335,12 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
                 swap(new_u_val, ac);
                 new_u_kind = ac_k;
                 set_is_upper_open(ac_o);
-            }
-            else {
+            } else {
                 swap(new_u_val, bd);
                 new_u_kind = bd_k;
                 set_is_upper_open(bd_o);
             }
-        }
-        else {
+        } else {
             // a < 0, a <= x, 0 <= c <= y <= d --> a*d <= x*y (uses the fact that c is not negative)
             // b > 0, x <= b, 0 <= c <= y <= d --> x*y <= b*d (uses the fact that c is not negative)
             lean_assert(i2.is_P());
@@ -363,8 +353,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
             round_to_plus_inf();
             mul(new_u_val, new_u_kind, b, b_k, d, d_k);
         }
-    }
-    else {
+    } else {
         lean_assert(i1.is_P());
         if (i2.is_N()) {
             // 0 <= a <= x <= b,   c <= y <= d <= 0  -->  x*y <= b*c (uses the fact that x is pos (a is not neg) or y is neg (d is not pos))
@@ -378,8 +367,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
             mul(new_l_val, new_l_kind, b, b_k, c, c_k);
             round_to_plus_inf();
             mul(new_u_val, new_u_kind, a, a_k, d, d_k);
-        }
-        else if (i2.is_M()) {
+        } else if (i2.is_M()) {
             // 0 <= a <= x <= b,  c <= y --> b*c <= x*y (uses the fact that a is not negative)
             // 0 <= a <= x <= b,  y <= d --> x*y <= b*d (uses the fact that a is not negative)
             set_is_lower_open(b_o || c_o);
@@ -389,8 +377,7 @@ interval<T> & interval<T>::operator*=(interval<T> const & o) {
             mul(new_l_val, new_l_kind, b, b_k, c, c_k);
             round_to_plus_inf();
             mul(new_u_val, new_u_kind, b, b_k, d, d_k);
-        }
-        else {
+        } else {
             lean_assert(i2.is_P());
             // 0 <= a <= x, 0 <= c <= y --> a*c <= x*y
             // x <= b, y <= d --> x*y <= b*d (uses the fact that x is pos (a is not negative) or y is pos (c is not negative))
@@ -424,8 +411,7 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
     if (i1.is_zero()) {
         // 0/other = 0 if other != 0
         // do nothing
-    }
-    else {
+    } else {
         T const & a = i1.m_lower; xnumeral_kind a_k = i1.lower_kind();
         T const & b = i1.m_upper; xnumeral_kind b_k = i1.upper_kind();
         T const & c = i2.m_lower; xnumeral_kind c_k = i2.lower_kind();
@@ -453,13 +439,11 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
                     lean_assert(d_o);
                     reset(new_u_val);
                     new_u_kind = XN_PLUS_INFINITY;
-                }
-                else {
+                } else {
                     round_to_plus_inf();
                     div(new_u_val, new_u_kind, a, a_k, d, d_k);
                 }
-            }
-            else {
+            } else {
                 // a <= x, a < 0,   0 < c <= y       -->  a/c <= x/y
                 // x <= b <= 0,     0 < c <= y <= d  -->         x/y <= b/d
                 lean_assert(i2.is_P1());
@@ -471,16 +455,14 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
                     lean_assert(c_o);
                     reset(new_l_val);
                     new_l_kind = XN_MINUS_INFINITY;
-                }
-                else {
+                } else {
                     round_to_minus_inf();
                     div(new_l_val, new_l_kind, a, a_k, c, c_k);
                 }
                 round_to_plus_inf();
                 div(new_u_val, new_u_kind, b, b_k, d, d_k);
             }
-        }
-        else if (i1.is_M()) {
+        } else if (i1.is_M()) {
             if (i2.is_N1()) {
                 // 0 < a <= x <= b < 0,  y <= d < 0   --> b/d <= x/y
                 // 0 < a <= x <= b < 0,  y <= d < 0   -->        x/y <= a/d
@@ -493,15 +475,13 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
                     reset(new_u_val);
                     new_l_kind = XN_MINUS_INFINITY;
                     new_u_kind = XN_PLUS_INFINITY;
-                }
-                else {
+                } else {
                     round_to_minus_inf();
                     div(new_l_val, new_l_kind, b, b_k, d, d_k);
                     round_to_plus_inf();
                     div(new_u_val, new_u_kind, a, a_k, d, d_k);
                 }
-            }
-            else {
+            } else {
                 // 0 < a <= x <= b < 0, 0 < c <= y  --> a/c <= x/y
                 // 0 < a <= x <= b < 0, 0 < c <= y  -->        x/y <= b/c
                 lean_assert(i1.is_P1());
@@ -515,16 +495,14 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
                     reset(new_u_val);
                     new_l_kind = XN_MINUS_INFINITY;
                     new_u_kind = XN_PLUS_INFINITY;
-                }
-                else {
+                } else {
                     round_to_minus_inf();
                     div(new_l_val, new_l_kind, a, a_k, c, c_k);
                     round_to_plus_inf();
                     div(new_u_val, new_u_kind, b, b_k, c, c_k);
                 }
             }
-        }
-        else {
+        } else {
             lean_assert(i1.is_P());
             if (i2.is_N1()) {
                 // b > 0,    x <= b,   c <= y <= d < 0    -->  b/d <= x/y
@@ -536,15 +514,13 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
                     lean_assert(d_o);
                     reset(new_l_val);
                     new_l_kind = XN_MINUS_INFINITY;
-                }
-                else {
+                } else {
                     round_to_minus_inf();
                     div(new_l_val, new_l_kind, b, b_k, d, d_k);
                 }
                 round_to_plus_inf();
                 div(new_u_val, new_u_kind, a, a_k, c, c_k);
-            }
-            else {
+            } else {
                 lean_assert(i2.is_P1());
                 // 0 <= a <= x,      0 < c <= y <= d    -->   a/d <= x/y
                 // b > 0     x <= b, 0 < c <= y         -->          x/y <= b/c
@@ -557,8 +533,7 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
                     lean_assert(c_o);
                     reset(new_u_val);
                     new_u_kind = XN_PLUS_INFINITY;
-                }
-                else {
+                } else {
                     round_to_plus_inf();
                     div(new_u_val, new_u_kind, b, b_k, c, c_k);
                 }
@@ -599,8 +574,7 @@ void interval<T>::inv() {
             reset(m_upper);
             set_is_upper_inf(true);
             set_is_upper_open(true);
-        }
-        else {
+        } else {
             round_to_plus_inf();
             new_u_val = m_lower;
             inv(new_u_val);
@@ -612,8 +586,7 @@ void interval<T>::inv() {
         swap(m_lower, new_l_val);
         set_is_lower_inf(false);
         set_is_lower_open(new_l_open);
-    }
-    else if (is_N1()) {
+    } else if (is_N1()) {
         // x <= u < 0 --> 1/u <= 1/x
         // l <= x <= u < 0 --> 1/l <= 1/x (use lower and upper bounds)
         round_to_plus_inf();
@@ -629,8 +602,7 @@ void interval<T>::inv() {
             reset(m_lower);
             set_is_lower_open(true);
             set_is_lower_inf(true);
-        }
-        else {
+        } else {
             round_to_minus_inf();
             new_l_val = m_upper;
             inv(new_l_val);
@@ -642,8 +614,7 @@ void interval<T>::inv() {
         swap(m_upper, new_u_val);
         set_is_upper_inf(false);
         set_is_upper_open(new_u_open);
-    }
-    else {
+    } else {
         lean_unreachable();
     }
     lean_assert(check_invariant());
@@ -657,8 +628,7 @@ void interval<T>::power(unsigned n) {
         // a^1 = a
         // nothing to be done
         return;
-    }
-    else if (n % 2 == 0) {
+    } else if (n % 2 == 0) {
         if (is_lower_pos()) {
             // [l, u]^n = [l^n, u^n] if l > 0
             // 0 < l <= x      --> l^n <= x^n (lower bound guarantees that is positive)
@@ -671,8 +641,7 @@ void interval<T>::power(unsigned n) {
                 round_to_plus_inf();
                 power(m_upper, n);
             }
-        }
-        else if (is_upper_neg()) {
+        } else if (is_upper_neg()) {
             // [l, u]^n = [u^n, l^n] if u < 0
             // l <= x <= u < 0   -->  x^n <= l^n (use lower and upper bound -- need the fact that x is negative)
             // x <= u < 0        -->  u^n <= x^n
@@ -688,15 +657,13 @@ void interval<T>::power(unsigned n) {
 
             if (li) {
                 reset(m_upper);
-            }
-            else {
+            } else {
                 round_to_plus_inf();
                 power(m_upper, n);
             }
             m_upper_inf  = li;
             m_upper_open = lo;
-        }
-        else {
+        } else {
             // [l, u]^n = [0, max{l^n, u^n}] otherwise
             // we need both bounds to justify upper bound
             xnumeral_kind un1_kind = lower_kind();
@@ -713,8 +680,7 @@ void interval<T>::power(unsigned n) {
                 swap(m_upper, un1);
                 m_upper_inf  = (un1_kind == XN_PLUS_INFINITY);
                 m_upper_open = m_lower_open;
-            }
-            else {
+            } else {
                 swap(m_upper, un2);
                 m_upper_inf = (un2_kind == XN_PLUS_INFINITY);
             }
@@ -723,8 +689,7 @@ void interval<T>::power(unsigned n) {
             m_lower_inf  = false;
             m_lower_open = false;
         }
-    }
-    else {
+    } else {
         // Remark: when n is odd x^n is monotonic.
         if (!m_lower_inf)
             power(m_lower, n);
@@ -745,8 +710,7 @@ T a_div_x_n(T a, T const & x, unsigned n, bool to_plus_inf) {
     if (n == 1) {
         numeric_traits<T>::set_rounding(to_plus_inf);
         a /= x;
-    }
-    else {
+    } else {
         static thread_local T tmp;
         numeric_traits<T>::set_rounding(!to_plus_inf);
         tmp = x;
@@ -764,8 +728,7 @@ bool interval<T>::check_invariant() const {
     if (eq(m_lower, lower_kind(), m_upper, upper_kind())) {
         lean_assert(!is_lower_open());
         lean_assert(!is_upper_open());
-    }
-    else {
+    } else {
         lean_assert(lt(m_lower, lower_kind(), m_upper, upper_kind()));
     }
     return true;
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 0d6951556..d38bd28e2 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -50,8 +50,7 @@ expr mk_app(unsigned n, expr const * as) {
     if (is_app(arg0)) {
         n0    = num_args(arg0);
         new_n = n + n0 - 1;
-    }
-    else {
+    } else {
         new_n = n;
     }
     char * mem   = new char[sizeof(expr_app) + new_n*sizeof(expr)];
@@ -198,20 +197,22 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
     case expr_kind::Eq:      out << "(" << eq_lhs(a) << " = " << eq_rhs(a) << ")"; break;
     case expr_kind::Lambda:  out << "(fun " << abst_name(a) << " : " << abst_domain(a) << " => " << abst_body(a) << ")"; break;
     case expr_kind::Pi:
-        if (!is_arrow(a))
+        if (!is_arrow(a)) {
             out << "(pi " << abst_name(a) << " : " << abst_domain(a) << ", " << abst_body(a) << ")";
-        else if (!is_arrow(abst_domain(a)))
+        } else if (!is_arrow(abst_domain(a))) {
             out << abst_domain(a) << " -> " << abst_body(a);
-        else
+        } else {
             out << "(" << abst_domain(a) << ") -> " << abst_body(a);
+        }
         break;
     case expr_kind::Let:  out << "(let " << let_name(a) << " := " << let_value(a) << " in " << let_body(a) << ")"; break;
     case expr_kind::Type: {
         level const & l = ty_level(a);
-        if (l == level())
+        if (l == level()) {
             out << "Type";
-        else
+        } else {
             out << "(Type " << ty_level(a) << ")";
+        }
         break;
     }
     case expr_kind::Value: to_value(a).display(out); break;
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 980a536a4..e566c8db5 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -441,8 +441,7 @@ template<typename F> expr update_abst(expr const & e, F f) {
     if (!is_eqp(p.first, old_t) || !is_eqp(p.second, old_b)) {
         name const & n = abst_name(e);
         return is_pi(e) ? mk_pi(n, p.first, p.second) : mk_lambda(n, p.first, p.second);
-    }
-    else {
+    } else {
         return e;
     }
 }
diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp
index bf9cef03c..8daa27b77 100644
--- a/src/kernel/free_vars.cpp
+++ b/src/kernel/free_vars.cpp
@@ -108,8 +108,7 @@ expr lower_free_vars(expr const & e, unsigned d) {
         if (is_var(e) && var_idx(e) >= offset) {
             lean_assert(var_idx(e) >= offset + d);
             return mk_var(var_idx(e) - d);
-        }
-        else {
+        } else {
             return e;
         }
     };
@@ -122,8 +121,7 @@ expr lift_free_vars(expr const & e, unsigned d) {
     auto f = [=](expr const & e, unsigned offset) -> expr {
         if (is_var(e) && var_idx(e) >= offset) {
             return mk_var(var_idx(e) + d);
-        }
-        else {
+        } else {
             return e;
         }
     };
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index b946b37b3..840704ebb 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -121,8 +121,7 @@ level max(level const & l1, level const & l2) {
             return max_core(to_max(l1), to_max(l1));
         else
             return max_core(to_max(l1), l2);
-    }
-    else {
+    } else {
         if (is_max(l2))
             return max_core(l1, to_max(l2));
         else
diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp
index bc1d3a069..b1d208123 100644
--- a/src/kernel/normalize.cpp
+++ b/src/kernel/normalize.cpp
@@ -157,8 +157,7 @@ class normalize_fn {
                     if (i == n - 1)
                         return f;
                     i++;
-                }
-                else {
+                } else {
                     buffer<expr> new_args;
                     expr new_f = reify(f, k);
                     new_args.push_back(new_f);
diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp
index decd9e510..f402479a8 100644
--- a/src/kernel/type_check.cpp
+++ b/src/kernel/type_check.cpp
@@ -27,8 +27,7 @@ bool is_convertible_core(expr const & expected, expr const & given, environment
         if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) {
             e = &abst_body(*e);
             g = &abst_body(*g);
-        }
-        else {
+        } else {
             return false;
         }
     }
diff --git a/src/util/debug.cpp b/src/util/debug.cpp
index ad99e0c38..5837d6d67 100644
--- a/src/util/debug.cpp
+++ b/src/util/debug.cpp
@@ -96,8 +96,7 @@ void invoke_debugger() {
             buffer << "gdb -nw /proc/" << getpid() << "/exe " << getpid();
             if (system(buffer.str().c_str()) == 0) {
                 std::cerr << "continuing the execution...\n";
-            }
-            else {
+            } else {
                 std::cerr << "ERROR STARTING GDB...\n";
                 // forcing seg fault.
                 int * x = 0;
diff --git a/src/util/escaped.cpp b/src/util/escaped.cpp
index be32470e1..3c9a1abaf 100644
--- a/src/util/escaped.cpp
+++ b/src/util/escaped.cpp
@@ -16,8 +16,7 @@ char const * escaped::end() const {
         if (!m_trim_nl || *it != '\n') {
             ++it;
             e = it;
-        }
-        else {
+        } else {
             ++it;
         }
     }
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 93efff136..8f11bc96c 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -166,8 +166,7 @@ bool operator==(name const & a, name const & b) {
         if (i1->m_is_string) {
             if (strcmp(i1->m_str, i2->m_str) != 0)
                 return false;
-        }
-        else {
+        } else {
             if (i1->m_k != i2->m_k)
                 return false;
         }
@@ -194,8 +193,7 @@ int cmp(name::imp * i1, name::imp * i2) {
             int c = strcmp(i1->m_str, i2->m_str);
             if (c != 0)
                 return c;
-        }
-        else if (i1->m_k != i2->m_k) {
+        } else if (i1->m_k != i2->m_k) {
             return i1->m_k < i2->m_k ? -1 : 1;
         }
     }
@@ -227,23 +225,20 @@ static unsigned num_digits(unsigned k) {
 size_t name::size(char const * sep) const {
     if (m_ptr == nullptr) {
         return strlen(anonymous_str);
-    }
-    else {
+    } else {
         imp * i       = m_ptr;
         size_t sep_sz = strlen(sep);
         size_t r      = 0;
         while (true) {
             if (i->m_is_string) {
                 r += strlen(i->m_str);
-            }
-            else {
+            } else {
                 r += num_digits(i->m_k);
             }
             if (i->m_prefix) {
                 r += sep_sz;
                 i  = i->m_prefix;
-            }
-            else {
+            } else {
                 break;
             }
         }
diff --git a/src/util/numerics/mpbq.cpp b/src/util/numerics/mpbq.cpp
index 4c3c0f9c7..7114e0ed8 100644
--- a/src/util/numerics/mpbq.cpp
+++ b/src/util/numerics/mpbq.cpp
@@ -14,8 +14,7 @@ bool set(mpbq & a, mpq const & b) {
         numerator(a.m_num, b);
         a.m_k = 0;
         return true;
-    }
-    else {
+    } else {
         static thread_local mpz d;
         denominator(d, b);
         unsigned shift;
@@ -24,8 +23,7 @@ bool set(mpbq & a, mpq const & b) {
             a.m_k = shift;
             lean_assert(a == b);
             return true;
-        }
-        else {
+        } else {
             numerator(a.m_num, b);
             a.m_k = d.log2() + 1;
             return false;
@@ -49,13 +47,12 @@ void mpbq::normalize() {
 
 int cmp(mpbq const & a, mpbq const & b) {
     static thread_local mpz tmp;
-    if (a.m_k == b.m_k)
+    if (a.m_k == b.m_k) {
         return cmp(a.m_num, b.m_num);
-    else if (a.m_k < b.m_k) {
+    } else if (a.m_k < b.m_k) {
         mul2k(tmp, a.m_num, b.m_k - a.m_k);
         return cmp(tmp, b.m_num);
-    }
-    else {
+    } else {
         lean_assert(a.m_k > b.m_k);
         mul2k(tmp, b.m_num, a.m_k - b.m_k);
         return cmp(a.m_num, tmp);
@@ -66,8 +63,7 @@ int cmp(mpbq const & a, mpz const & b) {
     static thread_local mpz tmp;
     if (a.m_k == 0) {
         return cmp(a.m_num, b);
-    }
-    else {
+    } else {
         mul2k(tmp, b, a.m_k);
         return cmp(a.m_num, tmp);
     }
@@ -76,8 +72,7 @@ int cmp(mpbq const & a, mpz const & b) {
 int cmp(mpbq const & a, mpq const & b) {
     if (a.is_integer() && b.is_integer()) {
         return -cmp(b, a.m_num);
-    }
-    else {
+    } else {
         static thread_local mpz tmp1;
         static thread_local mpz tmp2;
         // tmp1 <- numerator(a)*denominator(b)
@@ -91,13 +86,11 @@ int cmp(mpbq const & a, mpq const & b) {
 mpbq & mpbq::operator+=(mpbq const & a) {
     if (m_k == a.m_k) {
         m_num += a.m_num;
-    }
-    else if (m_k < a.m_k) {
+    } else if (m_k < a.m_k) {
         mul2k(m_num, m_num, a.m_k - m_k);
         m_k    = a.m_k;
         m_num += a.m_num;
-    }
-    else {
+    } else {
         lean_assert(m_k > a.m_k);
         static thread_local mpz tmp;
         mul2k(tmp, a.m_num, m_k - a.m_k);
@@ -111,8 +104,7 @@ template<typename T>
 mpbq & mpbq::add_int(T const & a) {
     if (m_k == 0) {
         m_num += a;
-    }
-    else {
+    } else {
         lean_assert(m_k > 0);
         static thread_local mpz tmp;
         tmp = a;
@@ -128,13 +120,11 @@ mpbq & mpbq::operator+=(int a) { return add_int<int>(a); }
 mpbq & mpbq::operator-=(mpbq const & a) {
     if (m_k == a.m_k) {
         m_num -= a.m_num;
-    }
-    else if (m_k < a.m_k) {
+    } else if (m_k < a.m_k) {
         mul2k(m_num, m_num, a.m_k - m_k);
         m_k    = a.m_k;
         m_num -= a.m_num;
-    }
-    else {
+    } else {
         lean_assert(m_k > a.m_k);
         static thread_local mpz tmp;
         mul2k(tmp, a.m_num, m_k - a.m_k);
@@ -148,8 +138,7 @@ template<typename T>
 mpbq & mpbq::sub_int(T const & a) {
     if (m_k == 0) {
         m_num -= a;
-    }
-    else {
+    } else {
         lean_assert(m_k > 0);
         static thread_local mpz tmp;
         tmp = a;
@@ -167,8 +156,7 @@ mpbq & mpbq::operator*=(mpbq const & a) {
     if (m_k == 0 || a.m_k == 0) {
         m_k   += a.m_k;
         normalize();
-    }
-    else {
+    } else {
         m_k   += a.m_k;
     }
     return *this;
@@ -196,11 +184,9 @@ int mpbq::magnitude_lb() const {
     int s = m_num.sgn();
     if (s < 0) {
         return m_num.mlog2() - m_k + 1;
-    }
-    else if (s == 0) {
+    } else if (s == 0) {
         return 0;
-    }
-    else {
+    } else {
         lean_assert(s > 0);
         return m_num.log2() - m_k;
     }
@@ -210,11 +196,9 @@ int mpbq::magnitude_ub() const {
     int s = m_num.sgn();
     if (s < 0) {
         return m_num.mlog2() - m_k;
-    }
-    else if (s == 0) {
+    } else if (s == 0) {
         return 0;
-    }
-    else {
+    } else {
         lean_assert(s > 0);
         return m_num.log2() - m_k + 1;
     }
@@ -223,8 +207,7 @@ int mpbq::magnitude_ub() const {
 void mul2(mpbq & a) {
     if (a.m_k == 0) {
         mul2k(a.m_num, a.m_num, 1);
-    }
-    else {
+    } else {
         a.m_k--;
     }
 }
@@ -235,8 +218,7 @@ void mul2k(mpbq & a, unsigned k) {
     if (a.m_k < k) {
         mul2k(a.m_num, a.m_num, k - a.m_k);
         a.m_k = 0;
-    }
-    else {
+    } else {
         lean_assert(a.m_k >= k);
         a.m_k -= k;
     }
@@ -250,13 +232,11 @@ bool root_lower(mpbq & a, mpbq const & b, unsigned n) {
         a.m_k = b.m_k / n;
         a.normalize();
         return r;
-    }
-    else if (a.m_num.is_neg()) {
+    } else if (a.m_num.is_neg()) {
         a.m_k = b.m_k / n;
         a.normalize();
         return false;
-    }
-    else {
+    } else {
         a.m_k = b.m_k / n;
         a.m_k++;
         a.normalize();
@@ -270,14 +250,12 @@ bool root_upper(mpbq & a, mpbq const & b, unsigned n) {
         a.m_k = b.m_k / n;
         a.normalize();
         return r;
-    }
-    else if (a.m_num.is_neg()) {
+    } else if (a.m_num.is_neg()) {
         a.m_k = b.m_k / n;
         a.m_k++;
         a.normalize();
         return false;
-    }
-    else {
+    } else {
         a.m_k = b.m_k / n;
         a.normalize();
         return false;
@@ -322,8 +300,7 @@ bool lt_1div2k(mpbq const & a, unsigned k) {
     if (a.m_k <= k) {
         // since a.m_num >= 1
         return false;
-    }
-    else {
+    } else {
         lean_assert(a.m_k > k);
         static thread_local mpz tmp;
         tmp = 1;
@@ -335,11 +312,9 @@ bool lt_1div2k(mpbq const & a, unsigned k) {
 std::ostream & operator<<(std::ostream & out, mpbq const & v) {
     if (v.m_k == 0) {
         out << v.m_num;
-    }
-    else if (v.m_k == 1) {
+    } else if (v.m_k == 1) {
         out << v.m_num << "/2";
-    }
-    else {
+    } else {
         out << v.m_num << "/2^" << v.m_k;
     }
     return out;
@@ -349,8 +324,7 @@ void display_decimal(std::ostream & out, mpbq const & a, unsigned prec) {
     if (a.is_integer()) {
         out << a.m_num;
         return;
-    }
-    else {
+    } else {
         mpz two_k;
         mpz n1, v1;
         if (a.is_neg())
diff --git a/src/util/numerics/mpq.cpp b/src/util/numerics/mpq.cpp
index 96249c29b..e4c2b8fc7 100644
--- a/src/util/numerics/mpq.cpp
+++ b/src/util/numerics/mpq.cpp
@@ -20,8 +20,7 @@ mpq & mpq::operator=(mpbq const & b) {
 int cmp(mpq const & a, mpz const & b) {
     if (a.is_integer()) {
         return mpz_cmp(mpq_numref(a.m_val), mpq::zval(b));
-    }
-    else {
+    } else {
         static thread_local mpz tmp;
         mpz_mul(mpq::zval(tmp), mpq_denref(a.m_val), mpq::zval(b));
         return mpz_cmp(mpq_numref(a.m_val), mpq::zval(tmp));
@@ -79,8 +78,7 @@ extern void display(std::ostream & out, __mpz_struct const * v);
 std::ostream & operator<<(std::ostream & out, mpq const & v) {
     if (v.is_integer()) {
         display(out, mpq_numref(v.m_val));
-    }
-    else {
+    } else {
         display(out, mpq_numref(v.m_val));
         out << "/";
         display(out, mpq_denref(v.m_val));
@@ -113,7 +111,6 @@ void display_decimal(std::ostream & out, mpq const & a, unsigned prec) {
     }
     out << "?";
 }
-
 }
 
 void pp(lean::mpq const & v) { std::cout << v << std::endl; }
diff --git a/src/util/numerics/mpz.cpp b/src/util/numerics/mpz.cpp
index c9527d50e..254a5c628 100644
--- a/src/util/numerics/mpz.cpp
+++ b/src/util/numerics/mpz.cpp
@@ -35,8 +35,7 @@ bool mpz::is_power_of_two(unsigned & shift) const {
     if (mpz_popcount(m_val) == 1) {
         shift = log2();
         return true;
-    }
-    else {
+    } else {
         return false;
     }
 }
@@ -64,8 +63,7 @@ void display(std::ostream & out, __mpz_struct const * v) {
         char buffer[1024];
         mpz_get_str(buffer, 10, v);
         out << buffer;
-    }
-    else {
+    } else {
         std::unique_ptr<char> buffer(new char[sz]);
         mpz_get_str(buffer.get(), 10, v);
         out << buffer.get();
diff --git a/src/util/numerics/xnumeral.h b/src/util/numerics/xnumeral.h
index b59711b54..fed5abb92 100644
--- a/src/util/numerics/xnumeral.h
+++ b/src/util/numerics/xnumeral.h
@@ -94,12 +94,10 @@ void add(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b,
     if (ak != XN_NUMERAL) {
         numeric_traits<T>::reset(r);
         rk = ak;
-    }
-    else if (bk != XN_NUMERAL) {
+    } else if (bk != XN_NUMERAL) {
         numeric_traits<T>::reset(r);
         rk = bk;
-    }
-    else {
+    } else {
         r = a + b;
         rk = XN_NUMERAL;
     }
@@ -113,8 +111,7 @@ void sub(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b,
         lean_assert(bk != ak);
         numeric_traits<T>::reset(r);
         rk = ak;
-    }
-    else {
+    } else {
         switch (bk) {
         case XN_MINUS_INFINITY:
             numeric_traits<T>::reset(r);
@@ -137,15 +134,13 @@ void mul(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b,
     if (is_zero(a, ak) || is_zero(b, bk)) {
         numeric_traits<T>::reset(r);
         rk = XN_NUMERAL;
-    }
-    else if (is_infinite(ak) || is_infinite(bk)) {
+    } else if (is_infinite(ak) || is_infinite(bk)) {
         if (is_pos(a, ak) == is_pos(b, bk))
             rk = XN_PLUS_INFINITY;
         else
             rk = XN_MINUS_INFINITY;
         numeric_traits<T>::reset(r);
-    }
-    else {
+    } else {
         rk = XN_NUMERAL;
         r = a * b;
     }
@@ -158,21 +153,18 @@ void div(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b,
         lean_assert(!is_zero(b, bk));
         numeric_traits<T>::reset(r);
         rk = XN_NUMERAL;
-    }
-    else if (is_infinite(ak)) {
+    } else if (is_infinite(ak)) {
         lean_assert(!is_infinite(bk));
         if (is_pos(a, ak) == is_pos(b, bk))
             rk = XN_PLUS_INFINITY;
         else
             rk = XN_MINUS_INFINITY;
         numeric_traits<T>::reset(r);
-    }
-    else if (is_infinite(bk)) {
+    } else if (is_infinite(bk)) {
         lean_assert(!is_infinite(ak));
         numeric_traits<T>::reset(r);
         rk = XN_NUMERAL;
-    }
-    else {
+    } else {
         rk = XN_NUMERAL;
         r = a / b;
     }
@@ -200,8 +192,7 @@ template<typename T>
 bool eq(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) {
     if (ak == XN_NUMERAL) {
         return bk == XN_NUMERAL && a == b;
-    }
-    else {
+    } else {
         return ak == bk;
     }
 }
diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp
index 9e0ddd28a..caafcddca 100644
--- a/src/util/sexpr/sexpr.cpp
+++ b/src/util/sexpr/sexpr.cpp
@@ -227,13 +227,11 @@ std::ostream & operator<<(std::ostream & out, sexpr const & s) {
             curr = &tail(*curr);
             if (is_nil(*curr)) {
                 break;
-            }
-            else if (!is_cons(*curr)) {
+            } else if (!is_cons(*curr)) {
                 out << " . ";
                 out << *curr;
                 break;
-            }
-            else {
+            } else {
                 out << " ";
             }
         }
diff --git a/src/util/sexpr/sexpr_funcs.h b/src/util/sexpr/sexpr_funcs.h
index e7241f58e..080215d67 100644
--- a/src/util/sexpr/sexpr_funcs.h
+++ b/src/util/sexpr/sexpr_funcs.h
@@ -30,8 +30,7 @@ sexpr map(sexpr const & l, F f) {
     lean_assert(is_list(l));
     if (is_nil(l)) {
         return l;
-    }
-    else {
+    } else {
         lean_assert(is_cons(l));
         return sexpr(f(head(l)), map(tail(l), f));
     }
@@ -44,8 +43,7 @@ sexpr filter(sexpr const & l, P p) {
     lean_assert(is_list(l));
     if (is_nil(l)) {
         return l;
-    }
-    else {
+    } else {
         lean_assert(is_cons(l));
         if (p(head(l)))
             return sexpr(head(l), filter(tail(l), p));
@@ -61,8 +59,7 @@ T foldl(sexpr const & l, T init, BOP op) {
     lean_assert(is_list(l));
     if (is_nil(l)) {
         return init;
-    }
-    else {
+    } else {
         lean_assert(is_cons(l));
         return foldl(tail(l), op(init, head(l)), op);
     }
@@ -75,8 +72,7 @@ T foldr(sexpr const & l, T init, BOP op) {
     lean_assert(is_list(l));
     if (is_nil(l)) {
         return init;
-    }
-    else {
+    } else {
         lean_assert(is_cons(l));
         return op(head(l), foldr(tail(l), init, op));
     }
@@ -89,8 +85,7 @@ bool forall(sexpr const & l, P p) {
     lean_assert(is_list(l));
     if (is_nil(l)) {
         return true;
-    }
-    else {
+    } else {
         lean_assert(is_cons(l));
         return p(head(l)) && forall(tail(l), p);
     }
@@ -103,8 +98,7 @@ bool contains(sexpr const & l, P p) {
     lean_assert(is_list(l));
     if (is_nil(l)) {
         return false;
-    }
-    else {
+     } else {
         lean_assert(is_cons(l));
         return p(head(l)) || contains(tail(l), p);
     }