From 7240a1a6403c0532f2cef4f61e43d98dd8dbd42c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 25 Oct 2014 11:17:29 -0700
Subject: [PATCH] feat(kernel/inductive): add get_num_minor_premises and
 get_num_type_formers APIs

---
 src/kernel/inductive/inductive.cpp | 18 ++++++++++++++++++
 src/kernel/inductive/inductive.h   |  8 ++++++++
 2 files changed, 26 insertions(+)

diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index 05fb6245c..01aaca5a2 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -971,6 +971,24 @@ optional<unsigned> get_num_indices(environment const & env, name const & n) {
     }
 }
 
+optional<unsigned> get_num_type_formers(environment const & env, name const & n) {
+    if (auto decls = is_inductive_decl(env, n)) {
+        return some(length(std::get<2>(*decls)));
+    } else {
+        return optional<unsigned>();
+    }
+}
+
+optional<unsigned> get_num_minor_premises(environment const & env, name const & n) {
+    inductive_env_ext const & ext = get_extension(env);
+    if (auto it = ext.m_elim_info.find(get_elim_name(n))) {
+        unsigned num_Cs = *get_num_type_formers(env, n);
+        return some(it->m_num_ACe - it->m_num_params - num_Cs);
+    } else {
+        return optional<unsigned>();
+    }
+}
+
 optional<name> is_intro_rule(environment const & env, name const & n) {
     inductive_env_ext const & ext = get_extension(env);
     if (auto it = ext.m_intro_info.find(n))
diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h
index 39be660fe..19387f10e 100644
--- a/src/kernel/inductive/inductive.h
+++ b/src/kernel/inductive/inductive.h
@@ -72,6 +72,14 @@ bool is_elim_meta_app(type_checker & tc, expr const & e);
     If \c n is not an inductive datatype in \c env, then return none.
 */
 optional<unsigned> get_num_indices(environment const & env, name const & n);
+/** \brief Return the number of minor premises in the given inductive datatype.
+    If \c n is not an inductive datatype in \c env, then return none.
+*/
+optional<unsigned> get_num_minor_premises(environment const & env, name const & n);
+/** \brief Return the number of type formers in the given inductive datatype.
+    If \c n is not an inductive datatype in \c env, then return none.
+*/
+optional<unsigned> get_num_type_formers(environment const & env, name const & n);
 
 /** \brief Return the eliminator/recursor associated with an inductive datatype */
 name get_elim_name(name const & n);