From eae26cdfaed812646840f17bb08c7ad1d0bc5208 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 15 Nov 2015 11:35:55 -0800
Subject: [PATCH] feat(library/user_recursors): add get_num_minors

---
 src/library/user_recursors.cpp | 10 ++++++++++
 src/library/user_recursors.h   |  2 +-
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp
index 362b10e00..1cd8ba3d3 100644
--- a/src/library/user_recursors.cpp
+++ b/src/library/user_recursors.cpp
@@ -22,6 +22,16 @@ bool recursor_info::is_minor(unsigned pos) const {
     return true;
 }
 
+unsigned recursor_info::get_num_minors() const {
+    unsigned r = m_num_args;
+    lean_assert(r >= get_motive_pos());
+    r -= get_motive_pos();
+    lean_assert(m_major_pos >= get_first_index_pos());
+    lean_assert(r >= m_major_pos - get_first_index_pos() + 1);
+    r -= (m_major_pos - get_first_index_pos() + 1);
+    return r;
+}
+
 recursor_info::recursor_info(name const & r, name const & I, list<unsigned> const & univ_pos,
                              bool dep_elim, unsigned num_args, unsigned major_pos,
                              list<optional<unsigned>> const & params_pos, list<unsigned> const & indices_pos,
diff --git a/src/library/user_recursors.h b/src/library/user_recursors.h
index ec6a6f7ce..5b36b023d 100644
--- a/src/library/user_recursors.h
+++ b/src/library/user_recursors.h
@@ -42,13 +42,13 @@ public:
     unsigned get_motive_pos() const { return get_num_params(); }
     unsigned get_first_index_pos() const { return m_major_pos - get_num_indices(); }
     unsigned get_major_pos() const { return m_major_pos; }
-    /** \brief Return position of the recursor parameters in the major premise. */
     list<optional<unsigned>> const & get_params_pos() const { return m_params_pos; }
     /** \brief Return position of the recursor indices in the major premise. */
     list<unsigned> const & get_indices_pos() const { return m_indices_pos; }
     list<bool> const & get_produce_motive() const { return m_produce_motive; }
     bool has_dep_elim() const { return m_dep_elim; }
     bool is_minor(unsigned pos) const;
+    unsigned get_num_minors() const;
 
     void write(serializer & s) const;
     static recursor_info read(deserializer & d);