From 7f142ac7e33538bb758be1a37f3078bd94c9e87b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 3 Aug 2019 10:51:24 -0700
Subject: [PATCH] chore(kernel/expr): hide `get_weight` and `get_depth`

---
 src/kernel/expr.h          | 4 ----
 src/library/expr_lt.cpp    | 8 --------
 src/library/type_context.h | 2 +-
 3 files changed, 1 insertion(+), 13 deletions(-)

diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index fb6ebeb811..0585820161 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -145,10 +145,6 @@ bool has_univ_mvar(expr const & e);
 inline bool has_mvar(expr const & e) { return has_expr_mvar(e) || has_univ_mvar(e); }
 bool has_fvar(expr const & e);
 bool has_univ_param(expr const & e);
-unsigned expr_get_weight(object * e);
-inline unsigned get_weight(expr const & e) { return expr_get_weight(e.raw()); }
-unsigned expr_get_depth(object * e);
-inline unsigned get_depth(expr const & e) { return expr_get_depth(e.raw()); }
 unsigned expr_get_loose_bvar_range(object * e);
 inline unsigned get_loose_bvar_range(expr const & e) { return expr_get_loose_bvar_range(e.raw()); }
 
diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp
index 5214d6d968..2332b714a6 100644
--- a/src/library/expr_lt.cpp
+++ b/src/library/expr_lt.cpp
@@ -10,10 +10,6 @@ Author: Leonardo de Moura
 namespace lean {
 bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const * lctx) {
     if (is_eqp(a, b))                    return false;
-    unsigned wa = get_weight(a);
-    unsigned wb = get_weight(b);
-    if (wa < wb)                         return true;
-    if (wa > wb)                         return false;
     if (a.kind() != b.kind())            return a.kind() < b.kind();
     if (use_hash) {
         if (hash(a) < hash(b))           return true;
@@ -126,10 +122,6 @@ bool is_lt_no_level_params(levels const & as, levels const & bs) {
 
 bool is_lt_no_level_params(expr const & a, expr const & b) {
     if (is_eqp(a, b))                    return false;
-    unsigned wa = get_weight(a);
-    unsigned wb = get_weight(b);
-    if (wa < wb)                         return true;
-    if (wa > wb)                         return false;
     if (a.kind() != b.kind())            return a.kind() < b.kind();
     switch (a.kind()) {
     case expr_kind::Lit:
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 58d5d6e0c1..cc8127acc6 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -520,7 +520,7 @@ private:
     std::function<bool(name const & e)> const * m_transparency_pred{nullptr}; // NOLINT
 
     static bool is_equiv_cache_target(expr const & e1, expr const & e2) {
-        return !has_metavar(e1) && !has_metavar(e2) && (get_weight(e1) > 1 || get_weight(e2) > 1);
+        return !has_metavar(e1) && !has_metavar(e2) && (!is_atomic(e1) || !is_atomic(e2));
     }
     bool is_cached_equiv(expr const & e1, expr const & e2) {
         return is_equiv_cache_target(e1, e2) && m_cache->get_equiv(m_transparency_mode, e1, e2);