feat(library/definitional/util): add is_recursive_datatype auxiliary function

src/library/definitional/CMakeLists.txt

@@ -1,4 +1,4 @@
 add_library(definitional rec_on.cpp induction_on.cpp cases_on.cpp unit.cpp eq.cpp heq.cpp
-  no_confusion.cpp projection.cpp)
+  no_confusion.cpp util.cpp projection.cpp)
 
 target_link_libraries(definitional ${LEAN_LIBS})

src/library/definitional/util.cpp

@@ -0,0 +1,28 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/find_fn.h"
+#include "kernel/inductive/inductive.h"
+
+namespace lean {
+bool is_recursive_datatype(environment const & env, name const & n) {
+    optional<inductive::inductive_decls> decls = inductive::is_inductive_decl(env, n);
+    if (!decls)
+        return false;
+    for (inductive::inductive_decl const & decl : std::get<2>(*decls)) {
+        for (inductive::intro_rule const & intro : inductive::inductive_decl_intros(decl)) {
+            expr type = inductive::intro_rule_type(intro);
+            while (is_pi(type)) {
+                if (find(binding_domain(type), [&](expr const & e, unsigned) {
+                            return is_constant(e) && const_name(e) == n; }))
+                    return true;
+                type = binding_body(type);
+            }
+        }
+    }
+    return false;
+}
+}

src/library/definitional/util.h

@@ -0,0 +1,20 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+
+namespace lean {
+/** \brief Return true iff \c n is the name of a recursive datatype in \c env.
+    That is, it must be an inductive datatype AND contain a recursive constructor.
+
+    \remark Records are inductive datatypes, but they are not recursive.
+
+    \remerk For mutually indutive datatypes, \c n is considered recursive
+    if there is a constructor taking \c n.
+*/
+bool is_recursive_datatype(environment const & env, name const & n);
+}