diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index db67585b8..36c442489 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -1122,6 +1122,16 @@ static int environment_whnf(lua_State * L) { return push_expr(L, type_checker(to
 static int environment_normalize(lua_State * L) { return push_expr(L, normalize(to_environment(L, 1), to_expr(L, 2))); }
 static int environment_infer_type(lua_State * L) { return push_expr(L, type_checker(to_environment(L, 1)).infer(to_expr(L, 2))); }
 static int environment_type_check(lua_State * L) { return push_expr(L, type_checker(to_environment(L, 1)).check(to_expr(L, 2))); }
+static int environment_for_each(lua_State * L) {
+    environment const & env = to_environment(L, 1);
+    luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
+    env.for_each([&](definition const & d) {
+            lua_pushvalue(L, 2); // push user-fun
+            push_definition(L, d);
+            pcall(L, 1, 0, 0);
+        });
+    return 0;
+}
 
 static const struct luaL_Reg environment_m[] = {
     {"__gc",              environment_gc}, // never throws
@@ -1143,6 +1153,7 @@ static const struct luaL_Reg environment_m[] = {
     {"normalize",         safe_function<environment_normalize>},
     {"infer_type",        safe_function<environment_infer_type>},
     {"type_check",        safe_function<environment_type_check>},
+    {"for_each",          safe_function<environment_for_each>},
     {0, 0}
 };
 
diff --git a/tests/lua/env8.lua b/tests/lua/env8.lua
new file mode 100644
index 000000000..a326f124d
--- /dev/null
+++ b/tests/lua/env8.lua
@@ -0,0 +1,13 @@
+local env = environment()
+local nat = Const("nat")
+
+env = add_inductive(env,
+                    "nat", Type,
+                    "zero", nat,
+                    "succ", mk_arrow(nat, nat))
+
+-- Display all declarations in the environment
+env:for_each(function(d)
+                print(tostring(d:name()) .. " : " .. tostring(d:type()))
+             end
+)