diff --git a/src/api/lean_name.h b/src/api/lean_name.h
index 2e277a676..5ac7af94e 100644
--- a/src/api/lean_name.h
+++ b/src/api/lean_name.h
@@ -60,6 +60,21 @@ lean_bool lean_name_get_idx(lean_name n, unsigned * r, lean_exception * ex);
 */
 lean_bool lean_name_to_string(lean_name n, char const **r, lean_exception * ex);
 
+LEAN_DEFINE_TYPE(lean_list_name);
+
+/** \brief Create the empty list of names */
+lean_bool lean_list_name_mk_nil(lean_list_name * r, lean_exception * ex);
+/** \brief Create the list <tt>h :: t</tt> */
+lean_bool lean_list_name_mk_cons(lean_name h, lean_list_name t, lean_list_name * r, lean_exception * ex);
+/** \brief Delete/dispose the given list of names */
+void lean_list_name_del(lean_list_name l);
+/** \brief Return true iff the list is a "cons" (i.e., it is not the nil list) */
+lean_bool lean_list_name_is_cons(lean_list_name l);
+/** \brief Store in \c r the head of the given list */
+lean_bool lean_list_name_head(lean_list_name l, lean_name * r, lean_exception * ex);
+/** \brief Store in \c r the tail of the given list */
+lean_bool lean_list_name_tail(lean_list_name l, lean_list_name * r, lean_exception * ex);
+
 /*@}*/
 /*@}*/
 
diff --git a/src/api/name.cpp b/src/api/name.cpp
index 866856786..b82f24b2b 100644
--- a/src/api/name.cpp
+++ b/src/api/name.cpp
@@ -99,3 +99,39 @@ lean_bool lean_name_to_string(lean_name n, char const **r, lean_exception * ex)
     *r = mk_string(to_name_ref(n).to_string());
     LEAN_CATCH;
 }
+
+lean_bool lean_list_name_mk_nil(lean_list_name * r, lean_exception * ex) {
+    LEAN_TRY;
+    *r = of_list_name(new list<name>());
+    LEAN_CATCH;
+}
+
+lean_bool lean_list_name_mk_cons(lean_name h, lean_list_name t, lean_list_name * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(h);
+    check_nonnull(t);
+    *r = of_list_name(new list<name>(to_name_ref(h), to_list_name_ref(t)));
+    LEAN_CATCH;
+}
+
+void lean_list_name_del(lean_list_name l) {
+    delete to_list_name(l);
+}
+
+lean_bool lean_list_name_is_cons(lean_list_name l) {
+    return l && !is_nil(to_list_name_ref(l));
+}
+
+lean_bool lean_list_name_head(lean_list_name l, lean_name * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(l);
+    *r = of_name(new name(head(to_list_name_ref(l))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_list_name_tail(lean_list_name l, lean_list_name * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(l);
+    *r = of_list_name(new list<name>(tail(to_list_name_ref(l))));
+    LEAN_CATCH;
+}
diff --git a/src/api/name.h b/src/api/name.h
index 12d6156f2..d8a718b58 100644
--- a/src/api/name.h
+++ b/src/api/name.h
@@ -13,4 +13,8 @@ inline name * to_name(lean_name n) { return reinterpret_cast<name *>(n); }
 inline name const & to_name_ref(lean_name n) { return *reinterpret_cast<name *>(n); }
 inline lean_name of_name(name * n) { return reinterpret_cast<lean_name>(n); }
 void to_buffer(unsigned sz, lean_name const * ns, buffer<name> & r);
+
+inline list<name> * to_list_name(lean_list_name n) { return reinterpret_cast<list<name> *>(n); }
+inline list<name> const & to_list_name_ref(lean_list_name n) { return *reinterpret_cast<list<name> *>(n); }
+inline lean_list_name of_list_name(list<name> * n) { return reinterpret_cast<lean_list_name>(n); }
 }