diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 0c6e05f5a..a38e23033 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -30,7 +30,7 @@ expr replace_range(expr const & type, expr const & new_range) {
 }
 
 /** \brief Return the "arity" of the given type. The arity is the number of nested pi-expressions. */
-static unsigned get_arity(expr type) {
+unsigned get_arity(expr type) {
     unsigned r = 0;
     while (is_pi(type)) {
         type = binding_body(type);
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 4cb8d35b1..c2818ed2c 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -18,6 +18,8 @@ Author: Leonardo de Moura
 #include "kernel/expr_maps.h"
 
 namespace lean {
+/** \brief Return the "arity" of the given type. The arity is the number of nested pi-expressions. */
+unsigned get_arity(expr type);
 
 inline pair<expr, constraint_seq> to_ecs(expr const & e) { return mk_pair(e, empty_cs()); }
 inline pair<expr, constraint_seq> to_ecs(expr const & e, constraint const & c, constraint_seq const & cs) {