diff --git a/doc/lua/lua.md b/doc/lua/lua.md
new file mode 100644
index 000000000..2fed0b1aa
--- /dev/null
+++ b/doc/lua/lua.md
@@ -0,0 +1,44 @@
+# Lua API documentation
+
+We the [Lua](http://www.lua.org) script language to customize and
+extend [Lean](http://leanprover.net). This
+[link](http://www.lua.org/docs.html) is a good starting point for
+learning Lua. In this document, we focus on the Lean specific APIs.
+Most of Lean components are exposed in the Lua API.
+
+**Remark:** the script [md2lua.sh](md2lua.sh) extracts the Lua code
+examples from the `*.md` documentation files in this directory.
+
+## Hierarchical names
+
+In Lean, we use _hierarchical names_ for identifying configuration
+options, constants, and kernel objects. A hierarchical name is
+essentially a list of strings and integers.
+The following example demonstrates how to create and manipulate
+hierarchical names using the Lua API.
+
+```lua
+local x = name("x")    -- create a simple hierarchical name
+local y = name("y")
+-- In Lua, 'assert(p)' succeeds if 'p' does not evaluate to false (or nil)
+assert(x == name("x")) -- test if 'x' is equal to 'name("x")'
+assert(x ~= y)         -- '~=' is the not equal operator in Lua
+assert(x ~= "x")
+
+assert(is_name(x)) -- test whether argument is a hierarchical name or not.
+assert(not is_name("x"))
+
+local x1 = name(x, 1) -- x1 is a name composed of the string "x" and number 1
+assert(tostring(x1) == "x::1")
+assert(x1 ~= name("x::1"))  -- x1 is not equal to the string x::1
+assert(x1 == name("x", 1))
+
+local o = name("lean", "pp", "colors")
+-- The previous construct is syntax sugar for the following expression
+assert(o == name(name(name("lean"), "pp"), "colors"))
+
+assert(x < y) -- '<' is a total order on hierarchical names
+
+local h = x:hash() -- retrieve the hash code for 'x'
+assert(h ~= y:hash())
+```
diff --git a/doc/lua/md2lua.sh b/doc/lua/md2lua.sh
new file mode 100755
index 000000000..dd10fb7d5
--- /dev/null
+++ b/doc/lua/md2lua.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/awk -f
+BEGIN{ in_block = 0 }
+!/```/{ if (in_block == 1) print $0; else print "" }
+/```/{ in_block = 0; print "" }
+/```lua/{ in_block = 1; print "" }