diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 2d43da9901..eb2d1f1dd1 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -4,38 +4,138 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <algorithm>
 #include "util/sstream.h"
+#include "kernel/type_checker.h"
 #include "library/io_state_stream.h"
 #include "library/scoped_ext.h"
 #include "library/aliases.h"
+#include "library/locals.h"
 #include "frontends/lean/parser.h"
 
 namespace lean {
 static name g_raw("raw");
+static name g_llevel_curly(".{");
+static name g_rcurly("}");
+static name g_colon(":");
+
 static void check_atomic(name const & n) {
     if (!n.is_atomic())
         throw exception(sstream() << "invalid declaration name '" << n << "', identifier must be atomic");
 }
 
 environment universe_cmd(parser & p) {
-    if (p.curr_is_identifier()) {
-        name n = p.get_name_val();
-        check_atomic(n);
-        p.next();
-        environment env = p.env();
-        if (in_section(env)) {
-            p.add_local_level(n, mk_param_univ(n));
-        } else {
-            name const & ns = get_namespace(env);
-            name full_n  = ns + n;
-            env = env.add_universe(full_n);
-            if (!ns.is_anonymous())
-                env = add_alias(env, n, mk_global_univ(full_n));
-        }
-        return env;
+    name n = p.check_id_next("invalid universe declaration, identifier expected");
+    check_atomic(n);
+    environment env = p.env();
+    if (in_section(env)) {
+        p.add_local_level(n, mk_param_univ(n));
     } else {
-        throw parser_error("invalid universe declaration, identifier expected", p.cmd_pos());
+        name const & ns = get_namespace(env);
+        name full_n  = ns + n;
+        env = env.add_universe(full_n);
+        if (!ns.is_anonymous())
+            env = add_alias(env, n, mk_global_univ(full_n));
     }
+    return env;
+}
+
+static void check_in_section(parser const & p) {
+    if (!in_section(p.env()))
+        throw exception(sstream() << "invalid command, it must be used in a section");
+}
+
+static void parse_univ_params(parser & p, buffer<name> & ps) {
+    if (p.curr_is_token(g_llevel_curly)) {
+        p.next();
+        while (!p.curr_is_token(g_rcurly)) {
+            name l = p.check_id_next("invalid universe parameter, identifier expected");
+            p.add_local_level(l, mk_param_univ(l));
+            ps.push_back(l);
+        }
+        p.next();
+    }
+}
+
+struct local_scope_if_not_section {
+    parser & m_p;
+    local_scope_if_not_section(parser & p):m_p(p) {
+        if (!in_section(p.env()))
+            p.push_local_scope();
+    }
+    ~local_scope_if_not_section() {
+        if (!in_section(m_p.env()))
+            m_p.pop_local_scope();
+    }
+};
+
+static void update_parameters(buffer<name> & ls_buffer, name_set const & found, parser const & p) {
+    unsigned old_sz = ls_buffer.size();
+    found.for_each([&](name const & n) {
+            if (std::find(ls_buffer.begin(), ls_buffer.begin() + old_sz, n) == ls_buffer.begin() + old_sz)
+                ls_buffer.push_back(n);
+        });
+    std::sort(ls_buffer.begin(), ls_buffer.end(), [&](name const & n1, name const & n2) {
+            return *p.get_local_level_index(n1) < *p.get_local_level_index(n2);
+        });
+}
+
+environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi) {
+    name n = p.check_id_next("invalid declaration, identifier expected");
+    check_atomic(n);
+    buffer<name> ls_buffer;
+    buffer<parameter> ps;
+    if (p.curr_is_token(g_llevel_curly) && in_section(p.env()))
+        throw parser_error("invalid declaration, axioms/parameters occurring in sections cannot be universe polymorphic", p.pos());
+    local_scope_if_not_section scope(p);
+    parse_univ_params(p, ls_buffer);
+    p.set_type_use_placeholder(false);
+    if (!p.curr_is_token(g_colon))
+        p.parse_binders(ps);
+    p.check_token_next(g_colon, "invalid declaration, ':' expected");
+    expr type = p.parse_scoped_expr(ps);
+    level_param_names ls;
+    if (in_section(p.env())) {
+        ls = to_level_param_names(collect_univ_params(type));
+    } else {
+        update_parameters(ls_buffer, collect_univ_params(type), p);
+        ls = to_list(ls_buffer.begin(), ls_buffer.end());
+    }
+    type = p.pi_abstract(ps, type);
+    type = p.elaborate(type, ls);
+    if (in_section(p.env())) {
+        p.add_local_expr(n, mk_local(n, n, type), bi);
+        return p.env();
+    } else {
+        environment env = p.env();
+        name const & ns = get_namespace(env);
+        name full_n  = ns + n;
+        if (is_axiom)
+            env = env.add(check(env, mk_axiom(full_n, ls, type)));
+        else
+            env = env.add(check(env, mk_var_decl(full_n, ls, type)));
+        if (!ns.is_anonymous())
+            env = add_alias(env, n, mk_constant(full_n));
+        return env;
+    }
+}
+environment variable_cmd(parser & p) {
+    return variable_cmd_core(p, false, binder_info());
+}
+environment axiom_cmd(parser & p)    {
+    return variable_cmd_core(p, true, binder_info());
+}
+environment implicit_variable_cmd(parser & p) {
+    check_in_section(p);
+    return variable_cmd_core(p, false, mk_implicit_binder_info());
+}
+environment implicit_axiom_cmd(parser & p) {
+    check_in_section(p);
+    return variable_cmd_core(p, true, mk_implicit_binder_info());
+}
+environment cast_variable_cmd(parser & p) {
+    check_in_section(p);
+    return variable_cmd_core(p, false, mk_cast_binder_info());
 }
 
 environment print_cmd(parser & p) {
@@ -58,14 +158,9 @@ environment section_cmd(parser & p) {
 }
 
 environment namespace_cmd(parser & p) {
-    if (p.curr_is_identifier()) {
-        name n = p.get_name_val();
-        check_atomic(n);
-        p.next();
-        return push_scope(p.env(), p.ios(), n);
-    } else {
-        throw parser_error("invalid namespace declaration, identifier expected", p.cmd_pos());
-    }
+    name n = p.check_id_next("invalid namespace declaration, identifier expected");
+    check_atomic(n);
+    return push_scope(p.env(), p.ios(), n);
 }
 
 environment end_scoped_cmd(parser & p) {
@@ -74,13 +169,28 @@ environment end_scoped_cmd(parser & p) {
     return pop_scope(p.env());
 }
 
+environment check_cmd(parser & p) {
+    expr e   = p.parse_expr();
+    level_param_names ls = to_level_param_names(collect_univ_params(e));
+    e = p.elaborate(e, ls);
+    expr type = type_checker(p.env()).check(e, ls);
+    p.regular_stream() << e << " : " << type << endl;
+    return p.env();
+}
+
 cmd_table init_cmd_table() {
     cmd_table r;
-    add_cmd(r, cmd_info("print",     "print a string", print_cmd));
-    add_cmd(r, cmd_info("universe",  "declare a global universe level", universe_cmd));
-    add_cmd(r, cmd_info("section",   "open a new section", section_cmd));
-    add_cmd(r, cmd_info("namespace", "open a new namespace", namespace_cmd));
-    add_cmd(r, cmd_info("end",       "close the current namespace/section", end_scoped_cmd));
+    add_cmd(r, cmd_info("print",        "print a string", print_cmd));
+    add_cmd(r, cmd_info("universe",     "declare a global universe level", universe_cmd));
+    add_cmd(r, cmd_info("section",      "open a new section", section_cmd));
+    add_cmd(r, cmd_info("namespace",    "open a new namespace", namespace_cmd));
+    add_cmd(r, cmd_info("end",          "close the current namespace/section", end_scoped_cmd));
+    add_cmd(r, cmd_info("variable",     "declare a new parameter", variable_cmd));
+    add_cmd(r, cmd_info("{variable}",   "declare a new implict parameter", implicit_variable_cmd));
+    add_cmd(r, cmd_info("[variable]",   "declare a new cast parameter", cast_variable_cmd));
+    add_cmd(r, cmd_info("axiom",        "declare a new axiom", axiom_cmd));
+    add_cmd(r, cmd_info("{axiom}",      "declare a new implicit axiom", implicit_axiom_cmd));
+    add_cmd(r, cmd_info("check",        "type check given expression, and display its type", check_cmd));
     return r;
 }
 
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index fa49d3102d..e93da92cda 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "frontends/lean/builtin_exprs.h"
+#include "frontends/lean/token_table.h"
 #include "frontends/lean/parser.h"
 
 namespace lean {
@@ -38,8 +39,8 @@ parse_table init_nud_table() {
 }
 
 parse_table init_led_table() {
-    parse_table r;
-    // TODO(Leo)
+    parse_table r(false);
+    r.add({transition("->", mk_expr_action(get_arrow_prec() + 1))}, mk_arrow(Var(0), Var(2)));
     return r;
 }
 }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 7d5cb5a4a2..70e75602ea 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -191,6 +191,14 @@ void parser::check_token_next(name const & tk, char const * msg) {
     next();
 }
 
+name parser::check_id_next(char const * msg) {
+    if (!curr_is_identifier())
+        throw parser_error(msg, pos());
+    name r = get_name_val();
+    next();
+    return r;
+}
+
 expr parser::mk_app(expr fn, expr arg, pos_info const & p) {
     return save_pos(::lean::mk_app(fn, arg), p);
 }
@@ -213,8 +221,8 @@ void parser::add_local_level(name const & n, level const & l) {
     m_local_level_decls.insert(n, local_level_entry(l, m_local_level_decls.size()));
 }
 
-void parser::add_local_expr(name const & n, expr const & e) {
-    m_local_decls.insert(n, local_entry(e, m_local_decls.size()));
+void parser::add_local_expr(name const & n, expr const & e, binder_info const & bi) {
+    m_local_decls.insert(n, local_entry(parameter(pos(), e, bi), m_local_decls.size()));
 }
 
 void parser::add_local(expr const & e) {
@@ -222,6 +230,22 @@ void parser::add_local(expr const & e) {
     add_local_expr(local_pp_name(e), e);
 }
 
+optional<unsigned> parser::get_local_level_index(name const & n) const {
+    auto it = m_local_level_decls.find(n);
+    if (it != m_local_level_decls.end())
+        return optional<unsigned>(it->second.second);
+    else
+        return optional<unsigned>();
+}
+
+optional<unsigned> parser::get_local_index(name const & n) const {
+    auto it = m_local_decls.find(n);
+    if (it != m_local_decls.end())
+        return optional<unsigned>(it->second.second);
+    else
+        return optional<unsigned>();
+}
+
 /** \brief Parse a sequence of identifiers <tt>ID*</tt>. Store the result in \c result. */
 void parser::parse_names(buffer<std::pair<pos_info, name>> & result) {
     while (curr_is_identifier()) {
@@ -372,6 +396,11 @@ expr parser::mk_Type() {
     }
 }
 
+expr parser::elaborate(expr const & e, level_param_names const &) {
+    // TODO(Leo):
+    return e;
+}
+
 /** \brief Parse <tt>ID ':' expr</tt>, where the expression represents the type of the identifier. */
 parameter parser::parse_binder_core(binder_info const & bi) {
     auto p  = pos();
@@ -576,7 +605,7 @@ expr parser::parse_id() {
     auto it1 = m_local_decls.find(id);
     // locals
     if (it1 != m_local_decls.end())
-        return copy_with_new_pos(it1->second.first, p);
+        return copy_with_new_pos(it1->second.first.m_local, p);
     buffer<level> lvl_buffer;
     auto p_lvl = pos();
     levels ls;
@@ -673,18 +702,15 @@ expr parser::parse_expr(unsigned rbp) {
     return left;
 }
 
-expr parser::parse_scoped_expr(unsigned num_locals, expr const * locals, unsigned rbp) {
-    local_decls::mk_scope scope(m_local_decls);
-    for (unsigned i = 0; i < num_locals; i++)
-        add_local(locals[i]);
-    return parse_expr(rbp);
-}
-
 expr parser::parse_scoped_expr(unsigned num_params, parameter const * ps, unsigned rbp) {
-    local_decls::mk_scope scope(m_local_decls);
-    for (unsigned i = 0; i < num_params; i++)
-        add_local(ps[i].m_local);
-    return parse_expr(rbp);
+    if (num_params == 0) {
+        return parse_expr(rbp);
+    } else {
+        local_decls::mk_scope scope(m_local_decls);
+        for (unsigned i = 0; i < num_params; i++)
+            add_local(ps[i].m_local);
+        return parse_expr(rbp);
+    }
 }
 
 expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda) {
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 4bad0b3639..356d9b5684 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -43,7 +43,7 @@ struct parser_error : public exception {
 struct interrupt_parser {};
 
 class parser {
-    typedef std::pair<expr, unsigned> local_entry;
+    typedef std::pair<parameter, unsigned> local_entry;
     typedef std::pair<level, unsigned> local_level_entry;
     typedef scoped_map<name, local_entry, name_hash, name_eq> local_decls;
     typedef scoped_map<name, local_level_entry, name_hash, name_eq> local_level_decls;
@@ -133,42 +133,6 @@ public:
     io_state const & ios() const { return m_ios; }
     script_state * ss() const { return m_ss; }
 
-    void parse_names(buffer<std::pair<pos_info, name>> & result);
-    unsigned parse_small_nat();
-
-    level parse_level(unsigned rbp = 0);
-
-    parameter parse_binder();
-    void parse_binders(buffer<parameter> & r);
-
-    expr parse_expr(unsigned rbp = 0);
-    expr parse_scoped_expr(unsigned num_locals, expr const * locals, unsigned rbp = 0);
-    expr parse_scoped_expr(unsigned num_params, parameter const * ps, unsigned rbp = 0);
-    expr parse_scoped_expr(buffer<parameter> & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
-    expr abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda = true);
-    expr abstract(buffer<parameter> const & ps, expr const & e, bool lambda = true) { return abstract(ps.size(), ps.data(), e, lambda); }
-
-    tactic parse_tactic(unsigned rbp = 0);
-
-    void push_local_scope();
-    void pop_local_scope();
-    void add_local_level(name const & n, level const & l);
-    void add_local_expr(name const & n, expr const & e);
-    void add_local(expr const & t);
-    /**
-       \brief Specify how the method mk_Type behaves. When <tt>set_type_use_placeholder(true)</tt>, then
-       it returns <tt>'Type.{_}'</tt>, where '_' is placeholder that instructs the Lean elaborator to
-       automalically infer a universe level expression for '_'. When <tt>set_type_use_placeholder(false)</tt>,
-       then it returns <tt>'Type.{l}'</tt>, where \c l is a fresh universe level parameter.
-       The new parameter is automatically added to \c m_local_level_decls.
-
-       \remark When the parse is created the flag is set to false.
-       \remark Before parsing a command, the parser automatically "caches" the current value, and
-       restores it after the command is parsed (or aborted).
-    */
-    void set_type_use_placeholder(bool f) { m_type_use_placeholder = f; }
-    expr mk_Type();
-
     /** \brief Return the current position information */
     pos_info pos() const { return pos_info(m_scanner.get_line(), m_scanner.get_pos()); }
     expr save_pos(expr e, pos_info p);
@@ -191,6 +155,8 @@ public:
     bool curr_is_token(name const & tk) const;
     /** \brief Check current token, and move to next characther, throw exception if current token is not \c tk. */
     void check_token_next(name const & tk, char const * msg);
+    /** \brief Check if the current token is an identifier, if it is return it and move to next token, otherwise throw an exception. */
+    name check_id_next(char const * msg);
 
     mpq const & get_num_val() const { return m_scanner.get_num_val(); }
     name const & get_name_val() const { return m_scanner.get_name_val(); }
@@ -201,6 +167,50 @@ public:
     regular regular_stream() const { return regular(env(), ios()); }
     diagnostic diagnostic_stream() const { return diagnostic(env(), ios()); }
 
+    void parse_names(buffer<std::pair<pos_info, name>> & result);
+    unsigned parse_small_nat();
+
+    level parse_level(unsigned rbp = 0);
+
+    parameter parse_binder();
+    void parse_binders(buffer<parameter> & r);
+
+    expr parse_expr(unsigned rbp = 0);
+    expr parse_scoped_expr(unsigned num_params, parameter const * ps, unsigned rbp = 0);
+    expr parse_scoped_expr(buffer<parameter> & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
+    expr abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda = true);
+    expr abstract(buffer<parameter> const & ps, expr const & e, bool lambda = true) { return abstract(ps.size(), ps.data(), e, lambda); }
+    expr lambda_abstract(buffer<parameter> const & ps, expr const & e) { return abstract(ps, e, true); }
+    expr pi_abstract(buffer<parameter> const & ps, expr const & e) { return abstract(ps, e, false); }
+
+    tactic parse_tactic(unsigned rbp = 0);
+
+    void push_local_scope();
+    void pop_local_scope();
+    struct local_scope { parser & m_p; local_scope(parser & p):m_p(p) { p.push_local_scope(); } ~local_scope() { m_p.pop_local_scope(); } };
+    void add_local_level(name const & n, level const & l);
+    void add_local_expr(name const & n, expr const & e, binder_info const & bi = binder_info());
+    void add_local(expr const & t);
+    /** \brief Position of the local level declaration named \c n in the sequence of local level decls. */
+    optional<unsigned> get_local_level_index(name const & n) const;
+    /** \brief Position of the local declaration named \c n in the sequence of local decls. */
+    optional<unsigned> get_local_index(name const & n) const;
+    /**
+       \brief Specify how the method mk_Type behaves. When <tt>set_type_use_placeholder(true)</tt>, then
+       it returns <tt>'Type.{_}'</tt>, where '_' is placeholder that instructs the Lean elaborator to
+       automalically infer a universe level expression for '_'. When <tt>set_type_use_placeholder(false)</tt>,
+       then it returns <tt>'Type.{l}'</tt>, where \c l is a fresh universe level parameter.
+       The new parameter is automatically added to \c m_local_level_decls.
+
+       \remark When the parse is created the flag is set to false.
+       \remark Before parsing a command, the parser automatically "caches" the current value, and
+       restores it after the command is parsed (or aborted).
+    */
+    void set_type_use_placeholder(bool f) { m_type_use_placeholder = f; }
+    expr mk_Type();
+
+    expr elaborate(expr const & e, level_param_names const &);
+
     /** parse all commands in the input stream */
     bool operator()() { return parse_commands(); }
 };
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index ad9d4aeee9..e837550be6 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -8,6 +8,8 @@ Author: Leonardo de Moura
 #include "frontends/lean/token_table.h"
 
 namespace lean {
+static unsigned g_arrow_prec = 25;
+unsigned get_arrow_prec() { return g_arrow_prec; }
 token_table add_command_token(token_table const & s, char const * token) {
     return insert(s, token, token_info(token));
 }
@@ -41,25 +43,28 @@ static char const * g_forall_unicode = "\u2200";
 static char const * g_arrow_unicode  = "\u2192";
 static char const * g_cup            = "\u2294";
 
-
 token_table init_token_table() {
     token_table t;
     char const * builtin[] = {"fun", "Pi", "let", "in", "have", "show", "by", "from", "(", ")", "{", "}", "[", "]",
-                              ".{", "Type", "...", ",", ".", ":", "calc", ":=", "--", "(*", "(--", "->",
+                              ".{", "Type", "...", ",", ".", ":", "calc", ":=", "--", "(*", "(--",
                               "proof", "qed", "private", "raw", "Bool", "+", g_cup, nullptr};
 
-    char const * commands[] = {"theorem", "axiom", "variable", "definition", "evaluate", "check",
-                               "print", "variables", "end", "namespace", "section", "import",
+    char const * commands[] = {"theorem", "axiom", "variable", "definition", "{axiom}", "{variable}", "[variable]",
+                               "variables", "{variables}", "[variables]",
+                               "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "abbreviation", "inductive", "record", "structure", "module", "universe",
                                nullptr};
 
     std::pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},
-         {g_arrow_unicode, "->"}, {nullptr, nullptr}};
+         {nullptr, nullptr}};
 
     std::pair<char const *, char const *> cmd_aliases[] =
         {{"parameter", "variable"}, {"parameters", "variables"}, {"lemma", "theorem"},
          {"hypothesis", "axiom"}, {"conjecture", "axiom"}, {"corollary", "theorem"},
+         {"{parameter}", "{variable}"}, {"{parameters}", "{variables}"},
+         {"[parameter]", "[variable]"}, {"[parameters]", "[variables]"},
+         {"{hypothesis}", "{axiom}"}, {"{conjecture}", "{axiom}"},
          {nullptr, nullptr}};
 
     auto it = builtin;
@@ -67,6 +72,7 @@ token_table init_token_table() {
         t = add_token(t, *it);
         it++;
     }
+    t = add_token(t, "->", get_arrow_prec());
 
     it = commands;
     while (*it) {
@@ -79,6 +85,7 @@ token_table init_token_table() {
         t = add_token(t, it2->first, it2->second);
         it2++;
     }
+    t = add_token(t, g_arrow_unicode, "->", get_arrow_prec());
 
     it2 = cmd_aliases;
     while (it2->first) {
diff --git a/src/frontends/lean/token_table.h b/src/frontends/lean/token_table.h
index fe56050a7c..28f7b850a9 100644
--- a/src/frontends/lean/token_table.h
+++ b/src/frontends/lean/token_table.h
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "util/lua.h"
 
 namespace lean {
+unsigned get_arrow_prec();
 class token_info {
     bool        m_command;
     name        m_value;
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index c5b11eaeed..8f916bc256 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -3,7 +3,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp
   normalize.cpp shared_environment.cpp module.cpp coercion.cpp
   private.cpp placeholder.cpp aliases.cpp level_names.cpp
-  update_declaration.cpp choice.cpp scoped_ext.cpp)
+  update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp)
 # hop_match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/library/locals.cpp b/src/library/locals.cpp
new file mode 100644
index 0000000000..3cc43398da
--- /dev/null
+++ b/src/library/locals.cpp
@@ -0,0 +1,65 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/name_set.h"
+#include "kernel/expr.h"
+#include "kernel/for_each_fn.h"
+
+namespace lean {
+void collect_univ_params_core(level const & l, name_set & r) {
+    for_each(l, [&](level const & l) {
+            if (!has_param(l))
+                return false;
+            if (is_param(l))
+                r.insert(param_id(l));
+            return true;
+        });
+}
+
+name_set collect_univ_params(expr const & e, name_set const & ls) {
+    if (!has_param_univ(e)) {
+        return ls;
+    } else {
+        name_set r = ls;
+        for_each(e, [&](expr const & e, unsigned) {
+                if (!has_param_univ(e)) {
+                    return false;
+                } else if (is_sort(e)) {
+                    collect_univ_params_core(sort_level(e), r);
+                } else if (is_constant(e)) {
+                    for (auto const & l : const_levels(e))
+                        collect_univ_params_core(l, r);
+                }
+                return true;
+            });
+        return r;
+    }
+}
+
+level_param_names to_level_param_names(name_set const & ls) {
+    level_param_names r;
+    ls.for_each([&](name const & n) {
+            r = level_param_names(n, r);
+        });
+    return r;
+}
+
+name_set collect_locals(expr const & e, name_set const & ls) {
+    if (!has_local(e)) {
+        return ls;
+    } else {
+        name_set r = ls;
+        for_each(e, [&](expr const & e, unsigned) {
+                if (!has_local(e))
+                    return false;
+                if (is_local(e))
+                    r.insert(mlocal_name(e));
+                return true;
+            });
+        return r;
+    }
+}
+}
diff --git a/src/library/locals.h b/src/library/locals.h
new file mode 100644
index 0000000000..f65a10ca2e
--- /dev/null
+++ b/src/library/locals.h
@@ -0,0 +1,14 @@
+/*
+Copyright (c) 2014 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_set.h"
+#include "kernel/expr.h"
+namespace lean {
+name_set collect_univ_params(expr const & e, name_set const & ls = name_set());
+name_set collect_locals(expr const & e, name_set const & ls = name_set());
+level_param_names to_level_param_names(name_set const & ls);
+}
diff --git a/tests/lean/t4.lean b/tests/lean/t4.lean
new file mode 100644
index 0000000000..cbfba7f1af
--- /dev/null
+++ b/tests/lean/t4.lean
@@ -0,0 +1,58 @@
+variable N : Type.{1}
+check N
+variable a : N
+check a
+check Bool → Bool
+variable F.{l} : Type.{l} → Type.{l}
+check F.{2}
+universe u
+check F.{u}
+variable vec.{l} (A : Type.{l}) (n : N) : Type.{l}
+variable f (a b : N) : N
+variable len.{l} (A : Type.{l}) (n : N) (v : vec.{l} A n) : N
+check f
+check len.{1}
+section
+   variable A  : Type
+   variable B  : Bool
+   hypothesis H : B
+   {parameter} C : Type
+   check B -> B
+   check A → A
+   check C
+end
+check A -- Error: A is part of the section
+
+variable R : Type → Type
+check R.{1 0}
+
+check fun x y : N, x
+
+namespace tst
+  variable N : Type.{2}
+  variable M : Type.{2}
+  print raw N -- Two possible interpretations N and tst.N
+  print raw tst.N -- Only one interpretation
+end
+print raw N -- Only one interpretation
+namespace foo
+  variable M : Type.{3}
+  print raw M -- Only one interpretation
+end
+check tst.M
+check foo.M
+namespace foo
+  check M
+end
+check M -- Error
+
+print "ok"
+(*
+local env = get_env()
+print("Declarations:")
+env:for_each_decl(function(d) print(d:name()) end)
+print("-------------")
+*)
+
+universe l_1
+variable T1 : Type -- T1 parameter is going to be called l_2
diff --git a/tests/lean/t4.lean.expected.out b/tests/lean/t4.lean.expected.out
new file mode 100644
index 0000000000..ab04626120
--- /dev/null
+++ b/tests/lean/t4.lean.expected.out
@@ -0,0 +1,34 @@
+N : Type
+a : N
+Bool -> Bool : Type
+F.{2} : Type.{2} -> Type.{2}
+F.{u} : Type.{u} -> Type.{u}
+f : N -> N -> N
+len.{1} : Pi (A : Type) (n : N) (v : vec.{1} A n), N
+B -> B : Bool
+A -> A : Type.{l_1}
+C : Type.{l_2}
+t4.lean:24:6: error: unknown identifier 'A'
+R.{1 0} : Type -> Bool
+fun (x : N) (y : N), x : N -> N -> N
+choice N tst.N
+tst.N
+N
+foo.M
+tst.M : Type.{2}
+foo.M : Type.{3}
+foo.M : Type.{3}
+t4.lean:47:6: error: unknown identifier 'M'
+ok
+Declarations:
+tst.M
+tst.N
+N
+a
+F
+R
+len
+vec
+f
+foo.M
+-------------