diff --git a/library/init/lean/default.lean b/library/init/lean/default.lean
index ba39834776..aba7a53ae8 100644
--- a/library/init/lean/default.lean
+++ b/library/init/lean/default.lean
@@ -9,3 +9,4 @@ import init.lean.frontend
 import init.lean.extern
 import init.lean.environment
 import init.lean.modifiers
+import init.lean.runtime
diff --git a/library/init/lean/runtime.lean b/library/init/lean/runtime.lean
new file mode 100644
index 0000000000..e5b04d5a67
--- /dev/null
+++ b/library/init/lean/runtime.lean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.core
+
+namespace Lean
+
+@[extern "lean_closure_max_args"]
+constant closureMaxArgsFn : Unit → Nat := default _
+
+def closureMaxArgs : Nat :=
+closureMaxArgsFn ()
+
+end Lean
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index b1e0b71972..c0a0072f8e 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -1953,6 +1953,13 @@ obj_res fixpoint6(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, o
     return r;
 }
 
+// =======================================
+// Runtime info
+
+extern "C" object * lean_closure_max_args(object *) {
+    return mk_nat_obj(static_cast<unsigned>(LEAN_CLOSURE_MAX_ARGS));
+}
+
 // =======================================
 // Debugging helper functions