From 2d90c7354645170db0301af7b60d222fe74d7a88 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 21 Aug 2016 15:47:31 -0700
Subject: [PATCH] chore(library/equations_compiler/util): add helper method

---
 src/library/equations_compiler/util.cpp | 6 +++++-
 src/library/equations_compiler/util.h   | 1 +
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp
index 49cfde8bde..80a74ba39e 100644
--- a/src/library/equations_compiler/util.cpp
+++ b/src/library/equations_compiler/util.cpp
@@ -150,9 +150,13 @@ bool eqns_env_interface::is_inductive(expr const & e) const {
     return is_inductive(const_name(e));
 }
 
+optional<name> eqns_env_interface::is_constructor(name const & n) const {
+    return inductive::is_intro_rule(m_env, n);
+}
+
 optional<name> eqns_env_interface::is_constructor(expr const & e) const {
     if (!is_constant(e)) return optional<name>();
-    return inductive::is_intro_rule(m_env, const_name(e));
+    return is_constructor(const_name(e));
 }
 
 unsigned eqns_env_interface::get_inductive_num_params(name const & n) const {
diff --git a/src/library/equations_compiler/util.h b/src/library/equations_compiler/util.h
index 9debbb777f..775a6abdf6 100644
--- a/src/library/equations_compiler/util.h
+++ b/src/library/equations_compiler/util.h
@@ -81,6 +81,7 @@ public:
 
     bool is_inductive(name const & n) const;
     bool is_inductive(expr const & e) const;
+    optional<name> is_constructor(name const & n) const;
     optional<name> is_constructor(expr const & e) const;
     unsigned get_inductive_num_params(name const & n) const;
     unsigned get_inductive_num_indices(name const & n) const;