From 34d5882b9ade9348e48ed8875df25c7dfa91df6a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Nov 2015 16:51:16 -0800
Subject: [PATCH] refactor(library/util): rename old is_eq_rec

---
 src/library/tactic/inversion_tactic.cpp | 4 ++--
 src/library/util.cpp                    | 2 +-
 src/library/util.h                      | 5 ++++-
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp
index bc290c2f3..1942b9cac 100644
--- a/src/library/tactic/inversion_tactic.cpp
+++ b/src/library/tactic/inversion_tactic.cpp
@@ -552,7 +552,7 @@ class inversion_tac {
         expr const & eq  = binding_domain(type);
         expr const & lhs = app_arg(app_fn(eq));
         expr const & rhs = app_arg(eq);
-        lean_assert(is_eq_rec(lhs));
+        lean_assert(is_eq_rec_core(lhs));
         // lhs is of the form  (eq.rec A s C a s p)
         // aux_eq is a term of type ((eq.rec A s C a s p) = a)
         auto aux_eq = apply_eq_rec_eq(m_tc, m_ios, to_list(hyps), lhs);
@@ -656,7 +656,7 @@ class inversion_tac {
                 eq   = mk_app(app_fn(app_fn(eq)), new_lhs, new_rhs);
                 type = update_binding(type, eq, binding_body(type));
             }
-            if (!m_proof_irrel && is_eq_rec(new_lhs)) {
+            if (!m_proof_irrel && is_eq_rec_core(new_lhs)) {
                 return intro_next_eq_rec(g, type);
             } else {
                 return intro_next_eq_simple(g, type);
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 332c95bd5..36478d064 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -575,7 +575,7 @@ expr mk_heq(type_checker & tc, expr const & lhs, expr const & rhs) {
     return mk_app(mk_constant(get_heq_name(), {lvl}), A, lhs, B, rhs);
 }
 
-bool is_eq_rec(expr const & e) {
+bool is_eq_rec_core(expr const & e) {
     expr const & fn = get_app_fn(e);
     return is_constant(fn) && const_name(fn) == get_eq_rec_name();
 }
diff --git a/src/library/util.h b/src/library/util.h
index 6195965b8..37ea8af4c 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -159,7 +159,10 @@ expr mk_subst(type_checker & tc, expr const & motive, expr const & x, expr const
 expr mk_subst(type_checker & tc, expr const & motive, expr const & xeqy, expr const & h);
 /** \brief Create an proof for x = y using subsingleton.elim (in standard mode) and is_trunc.is_hprop.elim (in HoTT mode) */
 expr mk_subsingleton_elim(type_checker & tc, expr const & h, expr const & x, expr const & y);
-bool is_eq_rec(expr const & e);
+
+/** \brief Return true iff \c e is a term of the form (eq.rec ....) */
+bool is_eq_rec_core(expr const & e);
+
 bool is_eq(expr const & e);
 bool is_eq(expr const & e, expr & lhs, expr & rhs);
 /** \brief Return true iff \c e is of the form (eq A a a) */