diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 42d32d4527..4eb1afc576 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -451,7 +451,6 @@ endfunction()
 add_subdirectory(tests/util)
 add_subdirectory(tests/kernel)
 add_subdirectory(tests/library)
-add_subdirectory(tests/frontends/lean)
 add_subdirectory(tests/shell)
 
 # Include style check
diff --git a/src/tests/frontends/lean/CMakeLists.txt b/src/tests/frontends/lean/CMakeLists.txt
deleted file mode 100644
index 4904e50842..0000000000
--- a/src/tests/frontends/lean/CMakeLists.txt
+++ /dev/null
@@ -1,9 +0,0 @@
-add_executable(lean_scanner scanner.cpp ${LEAN_OBJS})
-target_link_libraries(lean_scanner ${EXTRA_LIBS})
-add_exec_test(lean_scanner "lean_scanner")
-# add_executable(lean_parser parser.cpp)
-# target_link_libraries(lean_parser ${ALL_LIBS})
-# add_exec_test(lean_parser "lean_parser")
-# # add_executable(lean_pp pp.cpp)
-# target_link_libraries(lean_pp ${ALL_LIBS})
-# add_exec_test(lean_pp "lean_pp")
diff --git a/src/tests/frontends/lean/frontend.cpp b/src/tests/frontends/lean/frontend.cpp
deleted file mode 100644
index 85ef7f365c..0000000000
--- a/src/tests/frontends/lean/frontend.cpp
+++ /dev/null
@@ -1,225 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <vector>
-#include "util/test.h"
-#include "kernel/environment.h"
-#include "kernel/kernel_exception.h"
-#include "kernel/kernel.h"
-#include "kernel/abstract.h"
-#include "library/printer.h"
-#include "library/bin_op.h"
-#include "library/io_state_stream.h"
-#include "frontends/lean/frontend.h"
-#include "frontends/lean/operator_info.h"
-#include "frontends/lean/pp.h"
-#include "frontends/lua/register_modules.h"
-using namespace lean;
-
-static void tst1() {
-    environment env; io_state ios = init_frontend(env);
-    env->add_uvar_cnstr("tst");
-    environment c = env->mk_child();
-    lean_assert(c->get_uvar("tst") == env->get_uvar("tst"));
-    lean_assert(env->has_children());
-}
-
-static void tst2() {
-    operator_info op1 = infixl(name("and"), 10);
-    operator_info op2 = infixr(name("implies"), 20);
-    lean_assert(op1.get_precedence() == 10);
-    lean_assert(op1.get_fixity() == fixity::Infixl);
-    op1.add_expr(mk_and_fn());
-    operator_info op3 = infixl(name("+"), 10);
-    op3.add_expr(Const(name{"Int", "plus"}));
-    op3.add_expr(Const(name{"Real", "plus"}));
-    std::cout << op3.get_denotations() << "\n";
-    lean_assert(length(op3.get_denotations()) == 2);
-    operator_info op4 = op3.copy();
-    op4.add_expr(Const(name{"Complex", "plus"}));
-    std::cout << op4.get_denotations() << "\n";
-    lean_assert(length(op3.get_denotations()) == 2);
-    lean_assert(length(op4.get_denotations()) == 3);
-    lean_assert(op4.get_fixity() == fixity::Infixl);
-    lean_assert(op4.get_op_name() == op3.get_op_name());
-    lean_assert(prefix("tst", 20).get_fixity() == fixity::Prefix);
-    lean_assert(postfix("!", 20).get_fixity() == fixity::Postfix);
-    lean_assert(length(mixfixl({"if", "then", "else"}, 10).get_op_name_parts()) == 3);
-    lean_assert(mixfixc({"if", "then", "else", "endif"}, 10).get_fixity() == fixity::Mixfixc);
-    std::cout << mixfixc({"if", "then", "else", "endif"}, 10).get_op_name_parts() << "\n";
-    std::cout << op4 << "\n";
-    std::cout << op2 << "\n";
-    std::cout << mixfixc({"if", "then", "else", "endif"}, 10) << "\n";
-}
-
-static void tst3() {
-    environment env;
-    std::cout << "====================\n";
-    std::cout << env << "\n";
-}
-
-static void tst4() {
-    environment env; io_state ios = init_frontend(env);
-    formatter fmt = mk_pp_formatter(env);
-    context c;
-    c = extend(c, "x", Prop);
-    c = extend(c, "y", Prop);
-    c = extend(c, "x", Prop, Var(1));
-    c = extend(c, "x", Prop, Var(2));
-    c = extend(c, "z", Prop, Var(1));
-    c = extend(c, "x", Prop, Var(4));
-    std::cout << fmt(c) << "\n";
-}
-
-static void tst5() {
-    std::cout << "=================\n";
-    environment env; io_state ios = init_frontend(env);
-    formatter fmt = mk_pp_formatter(env);
-    env->add_var("A", Type());
-    env->add_var("x", Const("A"));
-    optional<object> obj = env->find_object("x");
-    lean_assert(obj);
-    lean_assert(obj->get_name() == "x");
-    std::cout << fmt(*obj) << "\n";
-    optional<object> obj2 = env->find_object("y");
-    lean_assert(!obj2);
-    try {
-        env->get_object("y");
-        lean_unreachable();
-    } catch (unknown_name_exception & ex) {
-        std::cout << ex.what() << " " << ex.get_name() << "\n";
-    }
-}
-
-class alien_cell : public neutral_object_cell {
-    unsigned m_data[128];
-public:
-    alien_cell() {}
-    unsigned & get_data(unsigned i) { return m_data[i]; }
-    virtual char const * keyword() const { return "alien"; }
-    virtual void write(serializer & ) const { lean_unreachable(); } // LCOV_EXCL_LINE
-};
-
-static void tst6() {
-    std::cout << "=================\n";
-    environment env; io_state ios = init_frontend(env);
-    env->add_neutral_object(new alien_cell());
-    formatter fmt = mk_pp_formatter(env);
-    std::cout << fmt(env) << "\n";
-}
-
-static void tst7() {
-    environment env; io_state ios = init_frontend(env);
-    formatter fmt = mk_pp_formatter(env);
-    std::cout << fmt(And(Const("x"), Const("y"))) << "\n";
-}
-
-static void tst8() {
-    environment env; io_state ios = init_frontend(env);
-    formatter fmt = mk_pp_formatter(env);
-    add_infixl(env, ios, "<-$->", 10, mk_refl_fn());
-    std::cout << fmt(*(env->find_object("trivial"))) << "\n";
-}
-
-static void tst9() {
-    environment env; io_state ios = init_frontend(env);
-    lean_assert(!env->has_children());
-    {
-        environment c = env->mk_child();
-        lean_assert(env->has_children());
-    }
-    lean_assert(!env->has_children());
-    env->add_uvar_cnstr("l", level()+1);
-    lean_assert(env->get_uvar("l") == level("l"));
-    try { env->get_uvar("l2"); lean_unreachable(); }
-    catch (exception &) {}
-    env->add_definition("x", Prop, True);
-    object const & obj = env->get_object("x");
-    lean_assert(obj.get_name() == "x");
-    lean_assert(is_bool(obj.get_type()));
-    lean_assert(obj.get_value() == True);
-    try { env->get_object("y"); lean_unreachable(); }
-    catch (exception &) {}
-    lean_assert(!env->find_object("y"));
-    env->add_definition("y", False);
-    lean_assert(is_bool(env->find_object("y")->get_type()));
-    lean_assert(env->has_object("y"));
-    lean_assert(!env->has_object("z"));
-    bool found = false;
-    std::for_each(env->begin_objects(), env->end_objects(), [&](object const & obj) { if (obj.has_name() && obj.get_name() == "y") found = true; });
-    lean_assert(found);
-    add_postfix(env, ios, "!", 10, Const("factorial"));
-    name parts[] = {"if", "then", "else"};
-    add_mixfixl(env, ios, 3, parts, 10, Const("if"));
-}
-
-static void tst10() {
-    environment env; io_state ios = init_frontend(env);
-    formatter fmt = mk_pp_formatter(env);
-    expr x = Const("xxxxxxxxxxxx");
-    expr y = Const("y");
-    expr z = Const("foo");
-    expr e = Let({{x, True}, {y, And({x, x, x, x, x, x, x, x})}, {z, And(x, y)}}, Or({x, x, x, x, x, x, x, x, x, z, z, z, z, z, z, z}));
-    std::cout << e << "\n";
-    std::cout << fmt(e) << "\n";
-}
-
-static void tst11() {
-    environment env; io_state ios = init_frontend(env);
-    expr A = Const("A");
-    env->add_var("g", Pi({A, Type()}, A >> (A >> A)));
-    lean_assert(!has_implicit_arguments(env, "g"));
-    mark_implicit_arguments(env, "g", {true, false, false});
-    lean_assert(has_implicit_arguments(env, "g"))
-        name gexp = get_explicit_version(env, "g");
-    lean_assert(env->find_object(gexp));
-    lean_assert(env->find_object("g")->get_type() == env->find_object(gexp)->get_type());
-    lean_assert(get_implicit_arguments(env, "g") == std::vector<bool>({true})); // the trailing "false" marks are removed
-    try {
-        mark_implicit_arguments(env, "g", {true, false, false});
-        lean_unreachable();
-    } catch (exception & ex) {
-        std::cout << "Expected error: " << ex.what() << std::endl;
-    }
-    env->add_var("s", Pi({A, Type()}, A >> (A >> A)));
-    try {
-        mark_implicit_arguments(env, "s", {true, true, true, true});
-        lean_unreachable();
-    } catch (exception & ex) {
-        std::cout << "Expected error: " << ex.what() << std::endl;
-    }
-    env->add_var(name("@h"), Pi({A, Type()}, A >> (A >> A)));
-    env->add_var("h", Pi({A, Type()}, A >> (A >> A)));
-    try {
-        mark_implicit_arguments(env, "h", {true, false, false});
-        lean_unreachable();
-    } catch (exception & ex) {
-        std::cout << "Expected error: " << ex.what() << std::endl;
-    }
-    try {
-        mark_implicit_arguments(env, "u", {true, false});
-        lean_unreachable();
-    } catch (exception & ex) {
-        std::cout << "Expected error: " << ex.what() << std::endl;
-    }
-}
-
-int main() {
-    save_stack_info();
-    register_modules();
-    tst1();
-    tst2();
-    tst3();
-    tst4();
-    tst5();
-    tst6();
-    tst7();
-    tst8();
-    tst9();
-    tst10();
-    tst11();
-    return has_violations() ? 1 : 0;
-}
diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp
deleted file mode 100644
index a35c455acc..0000000000
--- a/src/tests/frontends/lean/parser.cpp
+++ /dev/null
@@ -1,118 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <sstream>
-#include <memory>
-#include "util/test.h"
-#include "util/exception.h"
-#include "util/numerics/mpq.h"
-#include "kernel/kernel.h"
-#include "library/printer.h"
-#include "library/io_state_stream.h"
-#include "library/arith/arith.h"
-#include "frontends/lean/parser.h"
-#include "frontends/lean/frontend.h"
-#include "frontends/lean/pp.h"
-#include "frontends/lua/register_modules.h"
-using namespace lean;
-
-static void parse(environment const & env, io_state const & ios, char const * str) {
-    environment child = env->mk_child();
-    io_state ios_copy = ios;
-    std::istringstream in(str);
-    if (parse_commands(child, ios_copy, in, "[string]")) {
-        formatter fmt = mk_pp_formatter(env);
-        std::for_each(child->begin_local_objects(),
-                      child->end_local_objects(),
-                      [&](object const & obj) {
-                          std::cout << fmt(obj) << "\n";
-                          std::cout << obj << "\n";
-                      });
-    }
-}
-
-static void parse_error(environment const & env, io_state const & ios, char const * str) {
-    try {
-        parse(env, ios, str);
-        lean_unreachable();
-    } catch (exception & ex) {
-        std::cout << "expected error: " << ex.what() << "\n";
-    }
-}
-
-static void tst1() {
-    environment env; io_state ios = init_test_frontend(env);
-    parse(env, ios, "variable x : Prop variable y : Prop axiom H : x && y || x -> x");
-    parse(env, ios, "eval true && true");
-    parse(env, ios, "print true && false eval true && false");
-    parse(env, ios, "infixl 35 & : and print true & false & false eval true & false");
-    parse(env, ios, "notation 100 if _ then _ fi : implies print if true then false fi");
-    parse(env, ios, "print forall (A : Type), A -> A");
-    parse(env, ios, "check forall (A : Type), A -> A");
-}
-
-static void check(environment const & env, io_state & ios, char const * str, expr const & expected) {
-    std::istringstream in(str);
-    try {
-        expr got = parse_expr(env, ios, in, "[string]");
-        lean_assert(expected == got);
-    } catch (exception &) {
-        lean_unreachable();
-    }
-}
-
-static void tst2() {
-    environment env; io_state ios = init_test_frontend(env);
-    env->add_var("x", Prop);
-    env->add_var("y", Prop);
-    env->add_var("z", Prop);
-    expr x = Const("x"); expr y = Const("y"); expr z = Const("z");
-    check(env, ios, "x && y", And(x, y));
-    check(env, ios, "x && y || z", Or(And(x, y), z));
-    check(env, ios, "x || y && z", Or(x, And(y, z)));
-    check(env, ios, "x || y || x && z", Or(x, Or(y, And(x, z))));
-    check(env, ios, "x || y || x && z -> x && y", mk_arrow(Or(x, Or(y, And(x, z))), And(x, y)));
-    check(env, ios, "x ∨ y ∨ x ∧ z → x ∧ y", mk_arrow(Or(x, Or(y, And(x, z))), And(x, y)));
-    check(env, ios, "x→y→z→x", mk_arrow(x, mk_arrow(y, mk_arrow(z, x))));
-    check(env, ios, "x->y->z->x", mk_arrow(x, mk_arrow(y, mk_arrow(z, x))));
-    check(env, ios, "x->(y->z)->x", mk_arrow(x, mk_arrow(mk_arrow(y, z), x)));
-}
-
-static void tst3() {
-    environment env; io_state ios = init_test_frontend(env);
-    parse(env, ios, "help");
-    parse(env, ios, "help options");
-    parse_error(env, ios, "help print");
-    check(env, ios, "10.3", mk_real_value(mpq(103, 10)));
-    parse(env, ios, "variable f : Real -> Real. check f 10.3.");
-    parse(env, ios, "variable g : (Type 1) -> Type. check g Type");
-    parse_error(env, ios, "check fun .");
-    parse_error(env, ios, "definition foo .");
-    parse_error(env, ios, "check a");
-    parse_error(env, ios, "check U");
-    parse(env, ios, "variable h : Real -> Real -> Real. notation 10 [ _ ; _ ] : h. check [ 10.3 ; 20.1 ].");
-    parse_error(env, ios, "variable h : Real -> Real -> Real. notation 10 [ _ ; _ ] : h. check [ 10.3 | 20.1 ].");
-    parse_error(env, ios, "set_option pp::indent true");
-    parse(env, ios, "set_option pp::indent 10");
-    parse_error(env, ios, "set_option pp::colors foo");
-    parse_error(env, ios, "set_option pp::colors \"foo\"");
-    parse(env, ios, "set_option pp::colors true");
-    parse_error(env, ios, "notation 10 : Int::add");
-    parse_error(env, ios, "notation 10 _ : Int::add");
-    parse(env, ios, "notation 10 _ ++ _ : Int::add. eval 10 ++ 20.");
-    parse(env, ios, "notation 10 _ -+ : Int::neg. eval 10 -+");
-    parse(env, ios, "notation 30 -+ _ : Int::neg. eval -+ 10");
-    parse_error(env, ios, "10 + 30");
-}
-
-int main() {
-    save_stack_info();
-    register_modules();
-    tst1();
-    tst2();
-    tst3();
-    return has_violations() ? 1 : 0;
-}
diff --git a/src/tests/frontends/lean/pp.cpp b/src/tests/frontends/lean/pp.cpp
deleted file mode 100644
index c8afb6fd04..0000000000
--- a/src/tests/frontends/lean/pp.cpp
+++ /dev/null
@@ -1,117 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/test.h"
-#include "kernel/abstract.h"
-#include "kernel/kernel.h"
-#include "library/printer.h"
-#include "library/io_state_stream.h"
-#include "frontends/lean/frontend.h"
-#include "frontends/lean/pp.h"
-#include "frontends/lua/register_modules.h"
-using namespace lean;
-
-static expr mk_shared_expr(unsigned depth) {
-    expr f = Const("f");
-    expr a = Const("a");
-    expr r = a;
-    for (unsigned i = 0; i < depth; i++)
-        r = f(r, r);
-    return r;
-}
-
-static void tst1() {
-    environment env; io_state ios = init_frontend(env);
-    formatter fmt = mk_pp_formatter(env);
-    std::cout << "Basic printer\n";
-    std::cout << mk_shared_expr(10) << std::endl;
-    std::cout << "----------------------------\nPretty printer\n";
-    std::cout << fmt(mk_shared_expr(10)) << std::endl;
-}
-
-static void tst2() {
-    environment env; io_state ios = init_frontend(env);
-    formatter fmt = mk_pp_formatter(env);
-    expr a = Const("a");
-    expr t = Fun({a, Type()}, mk_shared_expr(10));
-    expr g = Const("g");
-    std::cout << fmt(g(t, t, t)) << std::endl;
-    formatter fmt2 = mk_pp_formatter(env);
-    std::cout << fmt2(g(t, t, t), options({"lean", "pp", "alias_min_weight"}, 100)) << std::endl;
-}
-
-static void tst3() {
-    environment env; io_state ios = init_frontend(env);
-    formatter fmt = mk_pp_formatter(env);
-    expr g = Const("g");
-    expr a = Const("\u03BA");
-    expr b = Const("\u03C1");
-    expr c = Const("\u03BD");
-    expr d = Const(name("\u03BD", 1u));
-    expr t = g(a, mk_shared_expr(5));
-    std::cout << "----------------\n";
-    std::cout << fmt(t) << "\n----------------\n";
-    std::cout << fmt(g(b, t)) << "\n----------------\n";
-    std::cout << fmt(g(c, b, t)) << "\n----------------\n";
-    std::cout << fmt(g(d, c, b, t)) << "\n";
-}
-
-static void tst4() {
-    environment env; io_state ios = init_frontend(env);
-    io_state const & s1 = ios;
-    io_state s2 = ios;
-    regular(s1) << And(Const("a"), Const("b")) << "\n";
-    regular(ios) << And(Const("a"), Const("b")) << "\n";
-    diagnostic(ios) << And(Const("a"), Const("b")) << "\n";
-    ios.set_option(name{"lean", "pp", "notation"}, false);
-    regular(ios) << And(Const("a"), Const("b")) << "\n";
-    regular(s1) << And(Const("a"), Const("b")) << "\n";
-    regular(s2) << And(Const("a"), Const("b")) << "\n";
-}
-
-static void tst5() {
-    environment env; io_state ios = init_frontend(env);
-    std::shared_ptr<string_output_channel> out(std::make_shared<string_output_channel>());
-    ios.set_regular_channel(out);
-    ios.set_option(name{"pp", "unicode"}, true);
-    ios.set_option(name{"lean", "pp", "notation"}, true);
-    regular(ios) << And(Const("a"), Const("b"));
-    lean_assert(out->str() == "a ∧ b");
-    ios.set_option(name{"lean", "pp", "notation"}, false);
-    regular(ios) << " " << And(Const("a"), Const("b"));
-    lean_assert(out->str() == "a ∧ b and a b");
-}
-
-static expr mk_deep(unsigned depth) {
-    if (depth == 0)
-        return Const("a");
-    else
-        return Const("f")(mk_deep(depth - 1));
-}
-
-static void tst6() {
-    environment env; io_state ios = init_frontend(env);
-    std::shared_ptr<string_output_channel> out(std::make_shared<string_output_channel>());
-    ios.set_regular_channel(out);
-    expr t = mk_deep(10);
-    ios.set_option(name{"lean", "pp", "max_depth"}, 5);
-    ios.set_option(name{"pp", "colors"}, false);
-    ios.set_option(name{"pp", "unicode"}, false);
-    regular(ios) << t;
-    lean_assert(out->str() == "f (f (f (f (f (...)))))");
-}
-
-int main() {
-    save_stack_info();
-    register_modules();
-    tst1();
-    tst2();
-    tst3();
-    tst4();
-    tst5();
-    tst6();
-    return has_violations() ? 1 : 0;
-}
diff --git a/src/tests/frontends/lean/scanner.cpp b/src/tests/frontends/lean/scanner.cpp
deleted file mode 100644
index 6e875c9567..0000000000
--- a/src/tests/frontends/lean/scanner.cpp
+++ /dev/null
@@ -1,223 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <sstream>
-#include <string>
-#include "runtime/exception.h"
-#include "util/test.h"
-#include "util/escaped.h"
-#include "frontends/lean/scanner.h"
-#include "frontends/lean/parser_config.h"
-#include "init/init.h"
-using namespace lean;
-
-#define tk token_kind
-
-static void scan(char const * str, environment const & env = environment()) {
-    std::istringstream in(str);
-    scanner s(in, "[string]");
-    while (true) {
-        tk k = s.scan(env);
-        if (k == tk::Eof)
-            break;
-        if (k == tk::Identifier)
-            std::cout << "id[" << s.get_name_val() << "]";
-        else if (k == tk::CommandKeyword)
-            std::cout << "cmd[" << s.get_token_info().value() << "]";
-        else if (k == tk::Keyword)
-            std::cout << "tk[" << s.get_token_info().value() << "]";
-        else if (k == tk::Decimal || k == tk::Numeral)
-            std::cout << "n[" << s.get_num_val() << "]";
-        else if (k == tk::String)
-            std::cout << "[\"" << escaped(s.get_str_val().c_str()) << "\"]";
-        std::cout << ":" << s.get_pos() << ":" << s.get_line() << " ";
-    }
-    std::cout << "\n";
-}
-
-static void scan_success(char const * str, environment const & env = environment()) {
-    try {
-        scan(str, env);
-    } catch (exception & ex) {
-        std::cout << "ERROR: " << ex.what() << "\n";
-        lean_unreachable();
-    }
-}
-
-static void scan_error(char const * str) {
-    try {
-        scan(str);
-        lean_unreachable();
-    } catch (exception & ex) {
-        std::cout << "expected error: " << ex.what() << "\n";
-    }
-}
-
-static void check(char const * str, std::initializer_list<tk> const & l,
-                  environment const & env = environment()) {
-    try {
-        auto it = l.begin();
-        std::istringstream in(str);
-        scanner s(in, "[string]");
-        while (true) {
-            tk k = s.scan(env);
-            if (k == tk::Eof) {
-                lean_assert(it == l.end());
-                return;
-            }
-            lean_assert(it != l.end());
-            lean_assert_eq(k, *it);
-            ++it;
-        }
-    } catch (exception & ex) {
-        std::cout << "ERROR: " << ex.what() << "\n";
-        lean_unreachable();
-    }
-}
-
-static void check_name(char const * str, name const & expected, environment const & env = environment()) {
-    std::istringstream in(str);
-    scanner s(in, "[string]");
-    tk k = s.scan(env);
-    lean_assert(k == tk::Identifier);
-    lean_assert(s.get_name_val() == expected);
-    lean_assert(s.scan(env) == tk::Eof);
-}
-
-static void check_keyword(char const * str, name const & expected, environment const & env = environment()) {
-    std::istringstream in(str);
-    scanner s(in, "[string]");
-    tk k = s.scan(env);
-    lean_assert(k == tk::Keyword);
-    lean_assert(s.get_token_info().value() == expected);
-    lean_assert(s.scan(env) == tk::Eof);
-}
-
-static void tst1() {
-    environment env;
-    token_table s = get_token_table(env);
-    env = add_token(env, "+", 0);
-    env = add_token(env, "=", 0);
-    scan_success("a..a");
-    check("Type.{0}", {tk::Keyword, tk::Keyword, tk::Numeral, tk::Keyword});
-    env = add_token(env, "ab+cde", 0);
-    env = add_token(env, "+cd", 0);
-    scan_success("ab+cd", env);
-    check("ab+cd", {tk::Identifier, tk::Keyword}, env);
-    scan_success("ab+cde", env);
-    check("ab+cde", {tk::Keyword}, env);
-    scan_success("Type.{0}");
-    scan_success("0.a a");
-    scan_success("0.");
-    scan_success("0..");
-    scan_success("fun");
-    scan_success("..");
-    scan_success("....");
-    scan_success("....\n..");
-    scan_success("a", env);
-    scan_success("a. b.c..");
-    scan_success(".. ..");
-    scan_success("....\n..");
-    scan_success("fun(x: forall A : Type, A -> A), x+1 = 2.0 λvalue.foo. . . a", env);
-}
-
-static void tst2() {
-    scan("x.name");
-    scan("x.foo");
-    check("x.name", {tk::Identifier});
-    check("fun (x : Prop), x", {tk::Keyword, tk::Keyword, tk::Identifier, tk::Keyword, tk::Identifier,
-                 tk::Keyword, tk::Keyword, tk::Identifier});
-    check_name("x10", name("x10"));
-    // check_name("x.10", name(name("x"), 10));
-    check_name("x.bla", name({"x", "bla"}));
-
-    scan_error("***");
-    environment env;
-    token_table s = mk_default_token_table();
-    env = add_token(env, "***", 0);
-    check_keyword("***", "***", env);
-    env = add_token(env, "+", 0);
-    check("x+y", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
-    check("-- testing", {});
-    check("/- testing -/", {});
-    check("/- /- testing\n -/ -/", {});
-    check(" 2.31  ", {tk::Decimal});
-    check("2.31", {tk::Decimal});
-    check(" 333 22", {tk::Numeral, tk::Numeral});
-    check("int -> int", {tk::Identifier, tk::Keyword, tk::Identifier});
-    check("int->int", {tk::Identifier, tk::Keyword, tk::Identifier});
-    check_keyword("->", "->");
-    env = add_token(env, "-+->", 0);
-    check("Int -+-> Int", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
-    check("x := 10", {tk::Identifier, tk::Keyword, tk::Numeral});
-    check("{x}", {tk::Keyword, tk::Identifier, tk::Keyword});
-    check("λ ∀ →", {tk::Keyword, tk::Keyword, tk::Keyword});
-    check_keyword("λ", "fun");
-    scan("theorem a : Prop axiom b : Int");
-    check("theorem a : Prop axiom b : Int", {tk::CommandKeyword, tk::Identifier, tk::Keyword, tk::Identifier,
-                tk::CommandKeyword, tk::Identifier, tk::Keyword, tk::Identifier});
-    scan("foo \"ttk\\\"\" : Int");
-    check("foo \"ttk\\\"\" : Int", {tk::Identifier, tk::String, tk::Keyword, tk::Identifier});
-    scan_error("\"foo");
-    scan("2.13 1.2 0.5");
-}
-
-static void tst3() {
-    scan_error("\"\\");
-    scan_error("\"\\a");
-    scan("\"\naaa\"");
-    scan_error("foo.* 01");
-    scan("10.0.");
-    scan("{ } . forall exists let in ∀ := _");
-}
-
-static void tst4(unsigned N) {
-    std::string big;
-    for (unsigned i = 0; i < N; i++)
-        big += "aaa ";
-    std::istringstream in(big);
-    environment env;
-    scanner s(in, "[string]");
-    unsigned i = 0;
-    while (true) {
-        tk k = s.scan(env);
-        if (k == tk::Eof)
-            break;
-        i++;
-    }
-    std::cout << i << "\n";
-}
-
-static void tst_id_escape() {
-    check_name("«a»", name("a"));
-    check_name("«a».b", name({"a", "b"}));
-    check_name("a.«b»", name({"a", "b"}));
-    check_name("a.«b».c", name({"a", "b", "c"}));
-
-    check_name("«a.b».c", name({"a.b", "c"}));
-    check_name("«a b».c", name({"a b", "c"}));
-    check_name("«a🍏b».c", name({"a🍏b", "c"}));
-
-    check_name("a«b»", "ab");
-    check_name("«a»b", "ab");
-
-    scan_error("«");
-    scan_error("«a");
-    scan_error("«a\nb»");
-    scan_error("a.«");
-}
-
-int main() {
-    save_stack_info();
-    initialize();
-    tst1();
-    tst2();
-    tst3();
-    tst4(100000);
-    tst_id_escape();
-    finalize();
-    return has_violations() ? 1 : 0;
-}