diff --git a/src/util/name_set.cpp b/src/util/name_set.cpp
index 15e270925e..9c0d5f0077 100644
--- a/src/util/name_set.cpp
+++ b/src/util/name_set.cpp
@@ -17,4 +17,30 @@ name mk_unique(name_set const & s, name const & suggestion) {
         i++;
     }
 }
+
+DECL_UDATA(name_set)
+static int mk_name_set(lua_State * L) { return push_name_set(L, name_set()); }
+static int name_set_insert(lua_State * L) { return push_name_set(L, insert(to_name_set(L, 1), to_name_ext(L, 2))); }
+static int name_set_contains(lua_State * L) { return push_boolean(L, to_name_set(L, 1).contains(to_name_ext(L, 2))); }
+static int name_set_erase(lua_State * L) { return push_name_set(L, erase(to_name_set(L, 1), to_name_ext(L, 2))); }
+
+static const struct luaL_Reg name_set_m[] = {
+    {"__gc",     name_set_gc}, // never throws
+    {"insert",   safe_function<name_set_insert>},
+    {"contains", safe_function<name_set_contains>},
+    {"erase",    safe_function<name_set_erase>},
+    {0, 0}
+};
+static void name_set_migrate(lua_State * src, int i, lua_State * tgt) { push_name_set(tgt, to_name_set(src, i)); }
+
+void open_name_set(lua_State * L) {
+    luaL_newmetatable(L, name_set_mt);
+    set_migrate_fn_field(L, -1, name_set_migrate);
+    lua_pushvalue(L, -1);
+    lua_setfield(L, -2, "__index");
+    setfuncs(L, name_set_m, 0);
+
+    SET_GLOBAL_FUN(mk_name_set,   "name_set");
+    SET_GLOBAL_FUN(name_set_pred, "is_name_set");
+}
 }
diff --git a/src/util/name_set.h b/src/util/name_set.h
index 04b89eccdc..d1cfcc0afe 100644
--- a/src/util/name_set.h
+++ b/src/util/name_set.h
@@ -7,11 +7,12 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/rb_tree.h"
 #include "util/name.h"
+#include "util/lua.h"
 namespace lean {
 typedef rb_tree<name, name_quick_cmp> name_set;
-/**
-   \brief Make a name that does not occur in \c s, based on
-   the given suggestion.
-*/
+/** \brief Make a name that does not occur in \c s, based on the given suggestion. */
 name mk_unique(name_set const & s, name const & suggestion);
+
+UDATA_DEFS_CORE(name_set)
+void open_name_set(lua_State * L);
 }
diff --git a/src/util/script_state.cpp b/src/util/script_state.cpp
index 4329398213..1c9033df29 100644
--- a/src/util/script_state.cpp
+++ b/src/util/script_state.cpp
@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "util/script_exception.h"
 #include "util/name.h"
 #include "util/name_generator.h"
+#include "util/name_set.h"
 #include "util/rb_map.h"
 #include "util/lean_path.h"
 
@@ -86,6 +87,7 @@ struct script_state::imp {
         open_exception(m_state);
         open_name(m_state);
         open_name_generator(m_state);
+        open_name_set(m_state);
         open_rb_map(m_state);
         open_extra(m_state);
 
diff --git a/tests/lua/ns1.lua b/tests/lua/ns1.lua
new file mode 100644
index 0000000000..692cd5e741
--- /dev/null
+++ b/tests/lua/ns1.lua
@@ -0,0 +1,12 @@
+local s = name_set()
+assert(not s:contains("a"))
+s = s:insert("a")
+assert(s:contains("a"))
+s = s:insert("b")
+assert(s:contains("a"))
+assert(s:contains("b"))
+local s2 = s:erase("a")
+assert(s:contains("a"))
+assert(s:contains("b"))
+assert(not s2:contains("a"))
+assert(s2:contains("b"))