From 54ec66709c1bdcebe6f8ebe88e3cc866b81b516f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Jun 2014 11:01:03 -0700
Subject: [PATCH] doc(doc/lua): add constant and function application API
 documentation

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 doc/lua/lua.md | 94 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 94 insertions(+)

diff --git a/doc/lua/lua.md b/doc/lua/lua.md
index e3ff3e01b..b8d12563d 100644
--- a/doc/lua/lua.md
+++ b/doc/lua/lua.md
@@ -503,3 +503,97 @@ assert(e1:kind()   == level_kind.Max)
 assert(e2:kind()   == level_kind.IMax)
 ```
 
+# Expressions
+
+In Lean, we have the following kind of expressions: constants,
+function applications, variables, lambdas, dependent function spaces
+(aka Pis), let expressions, and sorts (aka Type).
+There are three additional kinds of auxiliary
+expressions: local constants, metavariables, and macros.
+
+## Constants
+
+Constants are essentially references to declarations in the
+environment. We can create a variable using
+
+```lua
+local f = mk_constant("f")
+local a = Const("a")       -- Const is an alias for mk_constant
+assert(is_expr(f))         -- f is an expression
+assert(f:is_constant())    -- f is a constant
+```
+Lean supports universe polymorphism. When we define a constant,
+theorem or axiom, we can use universe level parameters.
+Thus, if a declaration `g` has two universe level parameters,
+we instantiate them when we create a reference to `g`.
+
+```lua
+local zero = level()
+local one  = zero+1
+local g01  = mk_constant("g", {zero, one})
+```
+
+The command `mk_constant` automatically applies coercions to level
+expressions. A numeral `n` is automatically converted into
+`level()+n`, and a string `s` into `mk_param_univ(s)`.
+
+```lua
+local g1l = mk_constant("g", {1, "l"})
+```
+
+The method `data()` retrieves the name and universe levels of a
+constant.
+
+```lua
+local gl1 = mk_constant("g", {"l", 1})
+assert(gl1:is_constant())
+local n, ls = gl1:data()
+assert(n == name("g"))
+assert(#ls == 2)
+assert(ls:head() == mk_param_univ("l"))
+assert(ls:tail():head() == level()+1)
+```
+
+## Function applications
+
+In Lean, the expression `f t` is a function application, where `f` is
+a function that is applied to `t`.
+
+```lua
+local f = Const("f")
+local t = Const("t")
+local a = f(t)        -- Creates the term `f t`
+assert(is_expr(a))
+assert(a:is_app())
+```
+
+The method `data()` retrieves the function and argument of an
+application. The methods `fn()` and `arg()` retrieve the function
+and argument respectively.
+
+```lua
+local f = Const("f")
+local t = Const("t")
+local a = f(t)
+assert(a:fn()  == f)
+assert(a:arg() == t)
+local g, b = a:data()
+assert(g == f)
+assert(b == t)
+```
+As usual, we write `f t s` to denote the expression
+`((f t) s)`. The Lua API provides a similar convenience.
+
+```lua
+local f = Const("f")
+local t = Const("t")
+local s = Const("s")
+local a = f(t, s)
+assert(a:fn() == f(t))
+assert(a:fn():fn() == f)
+assert(a:fn():arg() == t)
+assert(a:arg() == s)
+```
+
+
+