diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt
index 4ff20a2d2e..ea40d421c9 100644
--- a/src/api/CMakeLists.txt
+++ b/src/api/CMakeLists.txt
@@ -1,4 +1,4 @@
-add_library(api OBJECT string.cpp exception.cpp name.cpp options.cpp univ.cpp)
+add_library(api OBJECT string.cpp exception.cpp name.cpp options.cpp univ.cpp expr.cpp)
 
 FILE(GLOB LEAN_API_INCLUDE_FILES lean*.h)
 install(FILES ${LEAN_API_INCLUDE_FILES} DESTINATION include)
diff --git a/src/api/expr.cpp b/src/api/expr.cpp
new file mode 100644
index 0000000000..d2d17a8ace
--- /dev/null
+++ b/src/api/expr.cpp
@@ -0,0 +1,361 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "api/univ.h"
+#include "api/expr.h"
+#include "api/string.h"
+#include "api/exception.h"
+namespace lean {
+void to_buffer(unsigned sz, lean_expr const * ns, buffer<expr> & r) {
+    check_nonnull(ns);
+    for (unsigned i = 0; i < sz; i++) {
+        check_nonnull(ns[i]);
+        r.push_back(to_expr_ref(ns[i]));
+    }
+}
+}
+
+using namespace lean; // NOLINT
+
+lean_bool lean_expr_mk_var(unsigned i, lean_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    *r = of_expr(new expr(mk_var(i)));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_mk_sort(lean_univ u, lean_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(u);
+    *r = of_expr(new expr(mk_sort(to_level_ref(u))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_mk_const(lean_name n, lean_list_univ us, lean_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(n);
+    check_nonnull(us);
+    *r = of_expr(new expr(mk_constant(to_name_ref(n), to_list_level_ref(us))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_mk_app(lean_expr f, lean_expr a, lean_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(f);
+    check_nonnull(a);
+    *r = of_expr(new expr(mk_app(to_expr_ref(f), to_expr_ref(a))));
+    LEAN_CATCH;
+}
+
+static binder_info to_binder_info(lean_binder_kind k) {
+    switch (k) {
+    case LEAN_BINDER_DEFAULT:         return binder_info();
+    case LEAN_BINDER_IMPLICIT:        return mk_implicit_binder_info();
+    case LEAN_BINDER_STRICT_IMPLICIT: return mk_strict_implicit_binder_info();
+    case LEAN_BINDER_INST_IMPLICIT:   return mk_inst_implicit_binder_info();
+    case LEAN_BINDER_HIDDEN:          return mk_contextual_info(false);
+    }
+    lean_unreachable();
+}
+
+static lean_binder_kind of_binder_info(binder_info k) {
+    if (k.is_implicit())
+        return LEAN_BINDER_IMPLICIT;
+    else if (k.is_inst_implicit())
+        return LEAN_BINDER_INST_IMPLICIT;
+    else if (k.is_strict_implicit())
+        return LEAN_BINDER_STRICT_IMPLICIT;
+    else if (!k.is_contextual())
+        return LEAN_BINDER_HIDDEN;
+    else
+        return LEAN_BINDER_DEFAULT;
+}
+
+lean_bool lean_expr_mk_lambda(lean_name n, lean_expr t, lean_expr b, lean_binder_kind k, lean_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(n);
+    check_nonnull(t);
+    check_nonnull(b);
+    *r = of_expr(new expr(mk_lambda(to_name_ref(n), to_expr_ref(t), to_expr_ref(b), to_binder_info(k))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_mk_pi(lean_name n, lean_expr t, lean_expr b, lean_binder_kind k, lean_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(n);
+    check_nonnull(t);
+    check_nonnull(b);
+    *r = of_expr(new expr(mk_pi(to_name_ref(n), to_expr_ref(t), to_expr_ref(b), to_binder_info(k))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_mk_macro(lean_macro_def m, lean_list_expr args, lean_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(m);
+    check_nonnull(args);
+    buffer<expr> _args;
+    to_buffer(to_list_expr_ref(args), _args);
+    *r = of_expr(new expr(mk_macro(to_macro_definition_ref(m), _args.size(), _args.data())));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_mk_local(lean_name n, lean_expr t, lean_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(n);
+    check_nonnull(t);
+    *r = of_expr(new expr(mk_local(to_name_ref(n), to_expr_ref(t))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_mk_local_ext(lean_name n, lean_name pp_n, lean_expr t, lean_binder_kind k, lean_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(n);
+    check_nonnull(pp_n);
+    check_nonnull(t);
+    *r = of_expr(new expr(mk_local(to_name_ref(n), to_name_ref(pp_n), to_expr_ref(t), to_binder_info(k))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_mk_metavar(lean_name n, lean_expr t, lean_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(n);
+    check_nonnull(t);
+    *r = of_expr(new expr(mk_metavar(to_name_ref(n), to_expr_ref(t))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_to_string(lean_expr e, char const ** r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(e);
+    std::ostringstream out;
+    out << to_expr_ref(e);
+    *r = mk_string(out.str());
+    LEAN_CATCH;
+}
+
+void lean_expr_del(lean_expr e) {
+    delete to_expr(e);
+}
+
+void lean_macro_def_del(lean_macro_def m) {
+    delete to_macro_definition(m);
+}
+
+lean_expr_kind lean_expr_get_kind(lean_expr e) {
+    if (!e)
+        return LEAN_EXPR_VAR;
+    switch (to_expr_ref(e).kind()) {
+    case expr_kind::Var:       return LEAN_EXPR_VAR;
+    case expr_kind::Sort:      return LEAN_EXPR_SORT;
+    case expr_kind::Constant:  return LEAN_EXPR_CONST;
+    case expr_kind::Meta:      return LEAN_EXPR_META;
+    case expr_kind::Local:     return LEAN_EXPR_LOCAL;
+    case expr_kind::App:       return LEAN_EXPR_APP;
+    case expr_kind::Lambda:    return LEAN_EXPR_LAMBDA;
+    case expr_kind::Pi:        return LEAN_EXPR_PI;
+    case expr_kind::Macro:     return LEAN_EXPR_MACRO;
+    }
+    lean_unreachable();
+}
+
+lean_bool lean_expr_eq(lean_expr e1, lean_expr e2, lean_bool * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(e1);
+    check_nonnull(e2);
+    *r = to_expr_ref(e1) == to_expr_ref(e2);
+    LEAN_CATCH;
+}
+
+static void check_expr_kind(lean_expr e, lean_expr_kind k, char const * msg) {
+    check_nonnull(e);
+    if (lean_expr_get_kind(e) != k)
+        throw exception(msg);
+}
+
+lean_bool lean_expr_get_var_idx(lean_expr e, unsigned * i, lean_exception * ex) {
+    LEAN_TRY;
+    check_expr_kind(e, LEAN_EXPR_VAR, "invalid argument, variable expected");
+    *i = var_idx(to_expr_ref(e));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_get_sort_univ(lean_expr e, lean_univ * u, lean_exception * ex) {
+    LEAN_TRY;
+    check_expr_kind(e, LEAN_EXPR_SORT, "invalid argument, sort expected");
+    *u = of_level(new level(sort_level(to_expr_ref(e))));
+    LEAN_CATCH;
+}
+
+static void check_constant(lean_expr e) {
+    check_expr_kind(e, LEAN_EXPR_CONST, "invalid argument, constant expected");
+}
+
+lean_bool lean_expr_get_const_name(lean_expr e, lean_name * n, lean_exception * ex) {
+    LEAN_TRY;
+    check_constant(e);
+    *n = of_name(new name(const_name(to_expr_ref(e))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_get_const_univs(lean_expr e, lean_list_univ * us, lean_exception * ex) {
+    LEAN_TRY;
+    check_constant(e);
+    *us = of_list_level(new list<level>(const_levels(to_expr_ref(e))));
+    LEAN_CATCH;
+}
+
+static void check_app(lean_expr e) {
+    check_expr_kind(e, LEAN_EXPR_APP, "invalid argument, function application expected");
+}
+
+lean_bool lean_expr_get_app_fun(lean_expr e, lean_expr * f, lean_exception * ex) {
+    LEAN_TRY;
+    check_app(e);
+    *f = of_expr(new expr(app_fn(to_expr_ref(e))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_get_app_arg(lean_expr e, lean_expr * a, lean_exception * ex) {
+    LEAN_TRY;
+    check_app(e);
+    *a = of_expr(new expr(app_arg(to_expr_ref(e))));
+    LEAN_CATCH;
+}
+
+static void check_mlocal(lean_expr e) {
+    check_nonnull(e);
+    if (lean_expr_get_kind(e) != LEAN_EXPR_LOCAL && lean_expr_get_kind(e) != LEAN_EXPR_META)
+        throw exception("invalid argument, local constant or meta-variable expected");
+}
+
+static void check_local(lean_expr e) {
+    check_expr_kind(e, LEAN_EXPR_LOCAL, "invalid argument, local constant expected");
+}
+
+lean_bool lean_expr_get_mlocal_name(lean_expr e, lean_name * n, lean_exception * ex) {
+    LEAN_TRY;
+    check_mlocal(e);
+    *n = of_name(new name(mlocal_name(to_expr_ref(e))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_get_mlocal_type(lean_expr e, lean_expr * t, lean_exception * ex) {
+    LEAN_TRY;
+    check_mlocal(e);
+    *t = of_expr(new expr(mlocal_type(to_expr_ref(e))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_get_local_pp_name(lean_expr e, lean_name * n, lean_exception * ex) {
+    LEAN_TRY;
+    check_local(e);
+    *n = of_name(new name(local_pp_name(to_expr_ref(e))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_get_local_binder_kind(lean_expr e, lean_binder_kind * k, lean_exception * ex) {
+    LEAN_TRY;
+    check_local(e);
+    *k = of_binder_info(local_info(to_expr_ref(e)));
+    LEAN_CATCH;
+}
+
+static void check_binding(lean_expr e) {
+    check_nonnull(e);
+    if (lean_expr_get_kind(e) != LEAN_EXPR_PI && lean_expr_get_kind(e) != LEAN_EXPR_LAMBDA)
+        throw exception("invalid argument, lambda or Pi expression expected");
+}
+
+lean_bool lean_expr_get_binding_name(lean_expr e, lean_name * n, lean_exception * ex) {
+    LEAN_TRY;
+    check_binding(e);
+    *n = of_name(new name(binding_name(to_expr_ref(e))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_get_binding_domain(lean_expr e, lean_expr * d, lean_exception * ex) {
+    LEAN_TRY;
+    check_binding(e);
+    *d = of_expr(new expr(binding_domain(to_expr_ref(e))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_get_binding_body(lean_expr e, lean_expr * b, lean_exception * ex) {
+    LEAN_TRY;
+    check_binding(e);
+    *b = of_expr(new expr(binding_body(to_expr_ref(e))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_get_binding_binder_kind(lean_expr e, lean_binder_kind * k, lean_exception * ex) {
+    LEAN_TRY;
+    check_binding(e);
+    *k = of_binder_info(binding_info(to_expr_ref(e)));
+    LEAN_CATCH;
+}
+
+static void check_macro(lean_expr e) {
+    check_expr_kind(e, LEAN_EXPR_MACRO, "invalid argument, macro application expected");
+}
+
+lean_bool lean_expr_get_macro_def(lean_expr e, lean_macro_def * d, lean_exception * ex) {
+    LEAN_TRY;
+    check_macro(e);
+    *d = of_macro_definition(new macro_definition(macro_def(to_expr_ref(e))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_get_macro_args(lean_expr e, lean_list_expr * as, lean_exception * ex) {
+    LEAN_TRY;
+    check_macro(e);
+    buffer<expr> args;
+    args.append(macro_num_args(to_expr_ref(e)), macro_args(to_expr_ref(e)));
+    *as = of_list_expr(new list<expr>(to_list(args)));
+    LEAN_CATCH;
+}
+
+lean_bool lean_list_expr_mk_nil(lean_list_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    *r = of_list_expr(new list<expr>());
+    LEAN_CATCH;
+}
+
+lean_bool lean_list_expr_mk_cons(lean_expr h, lean_list_expr t, lean_list_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(h);
+    check_nonnull(t);
+    *r = of_list_expr(new list<expr>(to_expr_ref(h), to_list_expr_ref(t)));
+    LEAN_CATCH;
+}
+
+void lean_list_expr_del(lean_list_expr l) {
+    delete to_list_expr(l);
+}
+
+lean_bool lean_list_expr_is_cons(lean_list_expr l) {
+    return l && !is_nil(to_list_expr_ref(l));
+}
+
+lean_bool lean_list_expr_eq(lean_list_expr l1, lean_list_expr l2) {
+    return l1 && l2 && to_list_expr_ref(l1) == to_list_expr_ref(l2);
+}
+
+lean_bool lean_list_expr_head(lean_list_expr l, lean_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(l);
+    if (!lean_list_expr_is_cons(l))
+        throw lean::exception("invalid argument, non-nil list expected");
+    *r = of_expr(new expr(head(to_list_expr_ref(l))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_list_expr_tail(lean_list_expr l, lean_list_expr * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(l);
+    if (!lean_list_expr_is_cons(l))
+        throw lean::exception("invalid argument, non-nil list expected");
+    *r = of_list_expr(new list<expr>(tail(to_list_expr_ref(l))));
+    LEAN_CATCH;
+}
diff --git a/src/api/expr.h b/src/api/expr.h
new file mode 100644
index 0000000000..8476f3808c
--- /dev/null
+++ b/src/api/expr.h
@@ -0,0 +1,28 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/name.h"
+#include "kernel/expr.h"
+#include "api/exception.h"
+#include "api/options.h"
+#include "api/lean_name.h"
+#include "api/lean_univ.h"
+#include "api/lean_expr.h"
+namespace lean {
+inline expr * to_expr(lean_expr n) { return reinterpret_cast<expr *>(n); }
+inline expr const & to_expr_ref(lean_expr n) { return *reinterpret_cast<expr *>(n); }
+inline lean_expr of_expr(expr * n) { return reinterpret_cast<lean_expr>(n); }
+void to_buffer(unsigned sz, lean_expr const * ns, buffer<expr> & r);
+
+inline list<expr> * to_list_expr(lean_list_expr n) { return reinterpret_cast<list<expr> *>(n); }
+inline list<expr> const & to_list_expr_ref(lean_list_expr n) { return *reinterpret_cast<list<expr> *>(n); }
+inline lean_list_expr of_list_expr(list<expr> * n) { return reinterpret_cast<lean_list_expr>(n); }
+
+inline macro_definition * to_macro_definition(lean_macro_def n) { return reinterpret_cast<macro_definition *>(n); }
+inline macro_definition const & to_macro_definition_ref(lean_macro_def n) { return *reinterpret_cast<macro_definition *>(n); }
+inline lean_macro_def of_macro_definition(macro_definition * n) { return reinterpret_cast<lean_macro_def>(n); }
+}
diff --git a/src/api/lean.h b/src/api/lean.h
index 574aa63a68..666e05cad5 100644
--- a/src/api/lean.h
+++ b/src/api/lean.h
@@ -14,5 +14,6 @@ Author: Leonardo de Moura
 #include "lean_name.h"          // NOLINT
 #include "lean_options.h"       // NOLINT
 #include "lean_univ.h"          // NOLINT
+#include "lean_expr.h"          // NOLINT
 
 #endif
diff --git a/src/api/lean_expr.h b/src/api/lean_expr.h
new file mode 100644
index 0000000000..e80e5e5a4b
--- /dev/null
+++ b/src/api/lean_expr.h
@@ -0,0 +1,162 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#ifndef _LEAN_EXPR_H
+#define _LEAN_EXPR_H
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/**
+   \defgroup capi C API
+*/
+/*@{*/
+
+/**
+   @name Expression API
+*/
+/*@{*/
+
+LEAN_DEFINE_TYPE(lean_macro_def);
+LEAN_DEFINE_TYPE(lean_expr);
+LEAN_DEFINE_TYPE(lean_list_expr);
+
+typedef enum {
+    LEAN_EXPR_VAR,
+    LEAN_EXPR_SORT,
+    LEAN_EXPR_CONST,
+    LEAN_EXPR_LOCAL,
+    LEAN_EXPR_META,
+    LEAN_EXPR_APP,
+    LEAN_EXPR_LAMBDA,
+    LEAN_EXPR_PI,
+    LEAN_EXPR_MACRO,
+} lean_expr_kind;
+
+typedef enum {
+    LEAN_BINDER_DEFAULT,           // (x : A)
+    LEAN_BINDER_IMPLICIT,          // {x : A}
+    LEAN_BINDER_STRICT_IMPLICIT,   // {{x : A}}
+    LEAN_BINDER_INST_IMPLICIT,     // [x : A]
+    LEAN_BINDER_HIDDEN             // like (x : A) but not included in proof goals
+} lean_binder_kind;
+
+/** \brief Create a variable with de-Bruijn index \c i.
+    This is a bounded variable. */
+lean_bool lean_expr_mk_var(unsigned i, lean_expr * r, lean_exception * ex);
+/** \brief r := Type.{u} */
+lean_bool lean_expr_mk_sort(lean_univ u, lean_expr * r, lean_exception * ex);
+/** \brief Create a constant with name \c n and universe parameters <tt>us[0], ..., us[sz-1]</tt>,
+    and store the result in \c r. */
+lean_bool lean_expr_mk_const(lean_name n, lean_list_univ us, lean_expr * r, lean_exception * ex);
+/** \brief Create a function application, r := f a */
+lean_bool lean_expr_mk_app(lean_expr f, lean_expr a, lean_expr * r, lean_exception * ex);
+/** \brief Create a lambda abstraction, r := (fun n : t, b)
+    \remark The parameter \c k specifies the kind of binder annotation (i.e., it corresponds to (), {}, {{}}, [] decorations in the lean front-end) */
+lean_bool lean_expr_mk_lambda(lean_name n, lean_expr t, lean_expr b, lean_binder_kind k, lean_expr * r, lean_exception * ex);
+/** \brief Create a Pi abstraction, r := (Pi n : t, b)
+    \remark The parameter \c k specifies the kind of binder annotation (i.e., it corresponds to (), {}, {{}}, [] decorations in the lean front-end) */
+lean_bool lean_expr_mk_pi(lean_name n, lean_expr t, lean_expr b, lean_binder_kind k, lean_expr * r, lean_exception * ex);
+/** \brief Create a macro application */
+lean_bool lean_expr_mk_macro(lean_macro_def m, lean_list_expr args, lean_expr * r, lean_exception * ex);
+/** \brief Create a local constant with name \c n and type \c t, and store the result in \c r.
+    \remark We use local constants to represent free variables. */
+lean_bool lean_expr_mk_local(lean_name n, lean_expr t, lean_expr * r, lean_exception * ex);
+/** \brief Create a local constant with internal name \c n and pretty print name \c pp_n, and type \c t, and store the result in \c r.
+    \remark We use local constants to represent free variables.
+    \remark The parameter \c k specifies the kind of binder annotation (i.e., it corresponds to (), {}, {{}}, [] decorations in the lean front-end). */
+lean_bool lean_expr_mk_local_ext(lean_name n, lean_name pp_n, lean_expr t, lean_binder_kind k, lean_expr * r, lean_exception * ex);
+/** \brief Create a meta-variable (aka unification variable) with name \c n and type \c t, and store the result in \c r. */
+lean_bool lean_expr_mk_metavar(lean_name n, lean_expr t, lean_expr * r, lean_exception * ex);
+
+/** \brief Store in \c r a (crude) string representation of the given expression.
+    \remark \c r must be deleted using #lean_string_del.
+    \remark To use the nicer pretty printer, we have an API that also takes a lean_environment object as argument. */
+lean_bool lean_expr_to_string(lean_expr e, char const ** r, lean_exception * ex);
+/** \brief Delete/dispose the given expression. */
+void lean_expr_del(lean_expr e);
+/** \brief Delete/dispose the given macro definition. */
+void lean_macro_def_del(lean_macro_def m);
+/** \brief Return the kind of the given expression.
+    \remark Return LEAN_EXPR_VAR if e is null. */
+lean_expr_kind lean_expr_get_kind(lean_expr e);
+/** \brief Store \c lean_true in \c r iff the two given expressions are equal. */
+lean_bool lean_expr_eq(lean_expr e1, lean_expr e2, lean_bool * r, lean_exception * ex);
+
+/** \brief Store in \c i the de-Brujin index of the given variable.
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_VAR */
+lean_bool lean_expr_get_var_idx(lean_expr e, unsigned * i, lean_exception * ex);
+/** \brief Stgore in \c u the universe of the given sort.
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_SORT */
+lean_bool lean_expr_get_sort_univ(lean_expr e, lean_univ * u, lean_exception * ex);
+/** \brief Store in \c n the name the given constant.
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_CONST */
+lean_bool lean_expr_get_const_name(lean_expr e, lean_name * n, lean_exception * ex);
+/** \brief Store in \c us the universes parameters of the given constant.
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_CONST */
+lean_bool lean_expr_get_const_univs(lean_expr e, lean_list_univ * us, lean_exception * ex);
+/** \brief Store in \c f the function of the given function application.
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_APP */
+lean_bool lean_expr_get_app_fun(lean_expr e, lean_expr * f, lean_exception * ex);
+/** \brief Store in \c a the argument of the given function application.
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_APP */
+lean_bool lean_expr_get_app_arg(lean_expr e, lean_expr * a, lean_exception * ex);
+/** \brief Store in \c n the name the given local constant or meta-variable.
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_LOCAL || lean_expr_get_kind(e) == LEAN_EXPR_META */
+lean_bool lean_expr_get_mlocal_name(lean_expr e, lean_name * n, lean_exception * ex);
+/** \brief Store in \c t the type the given local constant or meta-variable.
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_LOCAL || lean_expr_get_kind(e) == LEAN_EXPR_META */
+lean_bool lean_expr_get_mlocal_type(lean_expr e, lean_expr * t, lean_exception * ex);
+/** \brief Store in \c n the pretty printing name the given local constant.
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_LOCAL */
+lean_bool lean_expr_get_local_pp_name(lean_expr e, lean_name * n, lean_exception * ex);
+/** \brief Store in \c k the binder_kind associated with the given local constant.
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_LOCAL */
+lean_bool lean_expr_get_local_binder_kind(lean_expr e, lean_binder_kind * k, lean_exception * ex);
+/** \brief Store in \c n the name associated with the given binding expression (i.e., lambda or Pi).
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_LAMBDA || lean_expr_get_kind(e) == LEAN_EXPR_PI */
+lean_bool lean_expr_get_binding_name(lean_expr e, lean_name * n, lean_exception * ex);
+/** \brief Store in \c d the domain of the given binding (i.e., lambda or Pi).
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_LAMBDA || lean_expr_get_kind(e) == LEAN_EXPR_PI */
+lean_bool lean_expr_get_binding_domain(lean_expr e, lean_expr * d, lean_exception * ex);
+/** \brief Store in \c b the body of the given binding (i.e., lambda or Pi).
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_LAMBDA || lean_expr_get_kind(e) == LEAN_EXPR_PI */
+lean_bool lean_expr_get_binding_body(lean_expr e, lean_expr * b, lean_exception * ex);
+/** \brief Store in \c k the binder_kind of the given binding (i.e., lambda or Pi).
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_LAMBDA || lean_expr_get_kind(e) == LEAN_EXPR_PI */
+lean_bool lean_expr_get_binding_binder_kind(lean_expr e, lean_binder_kind * k, lean_exception * ex);
+/** \brief Store in \c d the macro definition of the given macro application.
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_MACRO */
+lean_bool lean_expr_get_macro_def(lean_expr e, lean_macro_def * d, lean_exception * ex);
+/** \brief Store in \c as the arguments of the given macro application.
+    \pre lean_expr_get_kind(e) == LEAN_EXPR_MACRO */
+lean_bool lean_expr_get_macro_args(lean_expr e, lean_list_expr * as, lean_exception * ex);
+
+/** \brief Create the empty list of exprs */
+lean_bool lean_list_expr_mk_nil(lean_list_expr * r, lean_exception * ex);
+/** \brief Create the list <tt>h :: t</tt> */
+lean_bool lean_list_expr_mk_cons(lean_expr h, lean_list_expr t, lean_list_expr * r, lean_exception * ex);
+/** \brief Delete/dispose the given list of exprs */
+void lean_list_expr_del(lean_list_expr l);
+/** \brief Return true iff the list is a "cons" (i.e., it is not the nil list) */
+lean_bool lean_list_expr_is_cons(lean_list_expr l);
+/** \brief Return true iff the two given lists are equal */
+lean_bool lean_list_expr_eq(lean_list_expr n1, lean_list_expr n2);
+/** \brief Store in \c r the head of the given list
+    \pre lean_list_expr_is_cons(l) */
+lean_bool lean_list_expr_head(lean_list_expr l, lean_expr * r, lean_exception * ex);
+/** \brief Store in \c r the tail of the given list
+    \pre lean_list_expr_is_cons(l) */
+lean_bool lean_list_expr_tail(lean_list_expr l, lean_list_expr * r, lean_exception * ex);
+
+/*@}*/
+/*@}*/
+
+#ifdef __cplusplus
+};
+#endif
+#endif