diff --git a/src/util/name.cpp b/src/util/name.cpp
index 81bece740..8479beab9 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -498,6 +498,20 @@ name to_name_ext(lua_State * L, int idx) {
     }
 }
 
+optional<name> to_optional_name(lua_State * L, int idx) {
+    if (lua_isnil(L, idx))
+        return optional<name>();
+    else
+        return optional<name>(to_name_ext(L, idx));
+}
+
+int push_optional_name(lua_State * L, optional<name> const & n) {
+    if (n)
+        return push_name(L, *n);
+    else
+        return push_nil(L);
+}
+
 static int name_tostring(lua_State * L) { return push_string(L, to_name(L, 1).to_string().c_str()); }
 static int name_eq(lua_State * L) { return push_boolean(L, to_name(L, 1) == to_name(L, 2)); }
 static int name_lt(lua_State * L) { return push_boolean(L, to_name(L, 1) < to_name(L, 2)); }
diff --git a/src/util/name.h b/src/util/name.h
index 191c2d82f..1e716edf8 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include "util/lua.h"
 #include "util/serializer.h"
+#include "util/optional.h"
 #include "util/list.h"
 
 namespace lean {
@@ -166,6 +167,8 @@ inline deserializer & operator>>(deserializer & d, name & n) { n = read_name(d);
 
 UDATA_DEFS(name)
 name to_name_ext(lua_State * L, int idx);
+optional<name> to_optional_name(lua_State * L, int idx);
+int push_optional_name(lua_State * L, optional<name> const & n);
 bool is_list_name(lua_State * L, int idx);
 list<name> & to_list_name(lua_State * L, int idx);
 list<name> to_list_name_ext(lua_State * L, int idx);