chore: update stage0

2019-12-05 06:19:18 -08:00 · 2019-12-05 06:19:18 -08:00 · da844e231a
commit da844e231a
parent 4fe9179f19
33 changed files with 1061 additions and 10860 deletions
--- a/stage0/src/Init/Lean.lean
+++ b/stage0/src/Init/Lean.lean
@ -20,3 +20,4 @@ import Init.Lean.MetavarContext
 import Init.Lean.AuxRecursor
 import Init.Lean.Linter
 import Init.Lean.Meta
+import Init.Lean.Eval
--- a/stage0/src/Init/Lean/Data/KVMap.lean
+++ b/stage0/src/Init/Lean/Data/KVMap.lean
@ -25,6 +25,16 @@ def DataValue.beq : DataValue → DataValue → Bool

 instance DataValue.HasBeq : HasBeq DataValue := ⟨DataValue.beq⟩

+@[export lean_data_value_to_string]
+def DataValue.str : DataValue → String
+| DataValue.ofString v => v
+| DataValue.ofBool v   => toString v
+| DataValue.ofName v   => toString v
+| DataValue.ofNat v    => toString v
+| DataValue.ofInt v    => toString v
+
+instance DataValue.hasToString : HasToString DataValue := ⟨DataValue.str⟩
+
 instance string2DataValue : HasCoe String DataValue := ⟨DataValue.ofString⟩
 instance bool2DataValue   : HasCoe Bool DataValue   := ⟨DataValue.ofBool⟩
 instance name2DataValue   : HasCoe Name DataValue   := ⟨DataValue.ofName⟩
--- a/stage0/src/Init/Lean/Data/Options.lean
+++ b/stage0/src/Init/Lean/Data/Options.lean
@ -5,6 +5,7 @@ Authors: Sebastian Ullrich and Leonardo de Moura
 -/
 prelude
 import Init.System.IO
+import Init.Data.Array
 import Init.Data.ToString
 import Init.Lean.Data.KVMap

@ -30,6 +31,7 @@ IO.mkRef (mkNameMap OptionDecl)
@[init initOptionDeclsRef]
 private constant optionDeclsRef : IO.Ref OptionDecls := arbitrary _

+@[export lean_register_option]
 def registerOption (name : Name) (decl : OptionDecl) : IO Unit :=
 do decls ← optionDeclsRef.get;
   when (decls.contains name) $
@ -38,6 +40,13 @@ do decls ← optionDeclsRef.get;

 def getOptionDecls : IO OptionDecls := optionDeclsRef.get

+@[export lean_get_option_decls_array]
+def getOptionDeclsArray : IO (Array (Name × OptionDecl)) :=
+do decls ← getOptionDecls;
+   pure $ decls.fold
+    (fun (r : Array (Name × OptionDecl)) k v => r.push (k, v))
+    #[]
+
 def getOptionDecl (name : Name) : IO OptionDecl :=
 do decls ← getOptionDecls;
   (some decl) ← pure (decls.find name) | throw $ IO.userError ("unknown option '" ++ toString name ++ "'");
@ -69,4 +78,13 @@ do let ps := (entry.splitOn "=").map String.trim;
     unless val.isInt $ throw (IO.userError ("invalid Int option value '" ++ val ++ "'"));
     pure $ opts.setInt key val.toInt

+@[init] def verboseOption : IO Unit :=
+registerOption `verbose { defValue := true, group := "", descr := "disable/enable verbose messages" }
+
+@[init] def timeoutOption : IO Unit :=
+registerOption `timeout { defValue := DataValue.ofNat 0, group := "", descr := "the (deterministic) timeout is measured as the maximum of memory allocations (in thousands) per task, the default is unbounded" }
+
+@[init] def maxMemoryOption : IO Unit :=
+registerOption `maxMemory { defValue := DataValue.ofNat 2048, group := "", descr := "maximum amount of memory available for Lean in megabytes" }
+
 end Lean
--- a/stage0/src/Init/Lean/Eval.lean
+++ b/stage0/src/Init/Lean/Eval.lean
@ -0,0 +1,23 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+prelude
+import Init.System.IO
+import Init.Lean.Environment
+
+namespace Lean
+
+universe u
+
+/-- `HasEval` extension that gives access to the current environment & options.
+    The basic `HasEval` class is in the prelude and should not depend on these
+    types. -/
+class MetaHasEval (α : Type u) :=
+(eval : Environment → Options → α → IO Unit)
+
+instance MetaHasEvalOfHasEval {α : Type u} [HasEval α] : MetaHasEval α :=
+⟨fun env opts a => HasEval.eval a⟩
+
+end Lean
--- a/stage0/src/Init/Lean/Meta/Basic.lean
+++ b/stage0/src/Init/Lean/Meta/Basic.lean
@ -13,6 +13,7 @@ import Init.Lean.ReducibilityAttrs
 import Init.Lean.Util.Trace
 import Init.Lean.Meta.Exception
 import Init.Lean.Meta.DiscrTreeTypes
+import Init.Lean.Eval

 /-
 This module provides four (mutually dependent) goodies that are needed for building the elaborator and tactic frameworks.
@ -745,6 +746,16 @@ do mctx' ← getMCtx;
   modify $ fun s => { mctx := mctx, .. s };
   finally x (modify $ fun s => { mctx := mctx', .. s })

+instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
+⟨fun env opts x => do
+   match x { config := { opts := opts } } { env := env } with
+   | EStateM.Result.ok a s    => do
+     s.traceState.traces.forM $ fun m => IO.println $ format m;
+     MetaHasEval.eval s.env opts a
+   | EStateM.Result.error err s => do
+     s.traceState.traces.forM $ fun m => IO.println $ format m;
+     throw (IO.userError (toString err))⟩
+
 end Meta
 end Lean

--- a/stage0/src/Init/System/IO.lean
+++ b/stage0/src/Init/System/IO.lean
@ -282,6 +282,8 @@ do child ← IO.Proc.spawn { stdout := IO.process.stdio.piped, ..args },

 universe u

+namespace Lean
+
 /-- Typeclass used for presenting the output of an `#eval` command. -/
 class HasEval (α : Type u) :=
 (eval : α → IO Unit)
@ -295,3 +297,5 @@ instance IO.HasEval {α : Type} [HasEval α] : HasEval (IO α) :=
 -- special case: do not print `()`
 instance IOUnit.HasEval : HasEval (IO Unit) :=
 ⟨fun x => x⟩
+
+end Lean
--- a/stage0/src/frontends/lean/builtin_cmds.cpp
+++ b/stage0/src/frontends/lean/builtin_cmds.cpp
@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <algorithm>
 #include <string>
+#include <vector>
 #include "runtime/sstream.h"
 #include "runtime/compact.h"
 #include "util/timeit.h"
@ -325,29 +326,46 @@ static environment eval_cmd(parser & p) {
    if (has_synthetic_sorry(e))
        return p.env();

-    type_context_old tc(p.env(), transparency_mode::All);
+    type_context_old tc(p.env(), p.get_options());
    auto type = tc.infer(e);
+    std::vector<object *> args;

-    bool has_eval = false;
-
-    /* Check if resultant type has an instance of has_eval */
+    optional<expr> meta_eval_instance;
    try {
-        expr has_eval_type = mk_app(tc, "HasEval", type);
-        optional<expr> eval_instance = tc.mk_class_instance(has_eval_type);
-        if (eval_instance) {
-            /* Modify the 'program' to (has_eval.eval e) */
-            e             = mk_app(tc, {"HasEval", "eval"}, 3, type, *eval_instance, e);
-            type          = tc.infer(e);
-            has_eval      = true;
-        }
+        expr meta_has_eval_type = mk_app(tc, {"Lean", "MetaHasEval"}, type);
+        meta_eval_instance = tc.mk_class_instance(meta_has_eval_type);
    } catch (exception &) {}

-    if (!has_eval) {
-        // NOTE: HasRepr implies HasEval
-        throw exception("result type does not have an instance of type class 'HasRepr' or 'HasEval'");
+    if (meta_eval_instance) {
+        /* Modify the 'program' to (fun env opts => MetaHasEval.eval env opts e) */
+        expr env = tc.push_local("env", mk_const({"Lean", "Environment"}));
+        expr opts = tc.push_local("opts", mk_const({"Lean", "Options"}));
+        e = tc.mk_lambda(env, tc.mk_lambda(opts,
+                                           mk_app(tc, {"Lean", "MetaHasEval", "eval"}, 5,
+                                                  {type, *meta_eval_instance, env, opts, e})));
+        // run `Environment -> Options -> IO Unit`
+        args = { p.env().to_obj_arg(), p.get_options().to_obj_arg(), io_mk_world() };
+    } else {
+        optional<expr> eval_instance;
+        try {
+            expr has_eval_type = mk_app(tc, {"Lean", "HasEval"}, type);
+            eval_instance = tc.mk_class_instance(has_eval_type);
+        } catch (exception &) {}
+
+        if (eval_instance) {
+            /* Modify the 'program' to (HasEval.eval e) */
+            e = mk_app(tc, {"Lean", "HasEval", "eval"}, 3, type, *eval_instance, e);
+            // run `IO Unit`
+            args = { io_mk_world() };
+        } else {
+            // NOTE: HasRepr implies HasEval
+            // NOTE: could also mention MetaHasEval but probably shouldn't
+            throw exception("result type does not have an instance of type class 'HasRepr' or 'Lean.HasEval'");
+        }
    }

    name fn_name = "_main";
+    type = tc.infer(e);
    auto new_env = compile_expr(p.env(), p.get_options(), fn_name, ls, type, e, pos);

    auto out = p.mk_message(p.cmd_pos(), p.pos(), INFORMATION);
@ -355,16 +373,14 @@ static environment eval_cmd(parser & p) {
    scope_traces_as_messages scope_traces(p.get_stream_name(), p.cmd_pos());
    std::streambuf * saved_cout = std::cout.rdbuf(out.get_text_stream().get_stream().rdbuf());

-    // run `IO Unit`
-    object * args[] = { io_mk_world() };
    object_ref r;

    try {
        if (p.profiling()) {
            timeit timer(out.get_text_stream().get_stream(), "eval time");
-            r = object_ref(ir::run_boxed(new_env, fn_name, &args[0]));
+            r = object_ref(ir::run_boxed(new_env, fn_name, args.size(), &args[0]));
        } else {
-            r = object_ref(ir::run_boxed(new_env, fn_name, &args[0]));
+            r = object_ref(ir::run_boxed(new_env, fn_name, args.size(), &args[0]));
        }
    } catch (exception & ex) {
        std::cout.rdbuf(saved_cout);
--- a/stage0/src/library/compiler/ir_interpreter.cpp
+++ b/stage0/src/library/compiler/ir_interpreter.cpp
@ -167,11 +167,12 @@ type decl_type(decl const & b) { return cnstr_get_type(b, 2); }
 fn_body const & decl_fun_body(decl const & b) { lean_assert(decl_tag(b) == decl_kind::Fun); return cnstr_get_ref_t<fn_body>(b, 3); }

 extern "C" object * lean_ir_find_env_decl(object * env, object * n);
-option_ref<decl> find_env_decl(environment const & env, name const & n) {
+option_ref<decl> find_ir_decl(environment const & env, name const & n) {
    return option_ref<decl>(lean_ir_find_env_decl(env.to_obj_arg(), n.to_obj_arg()));
 }

 static string_ref * g_mangle_prefix = nullptr;
+static string_ref * g_boxed_suffix = nullptr;
 static string_ref * g_boxed_mangled_suffix = nullptr;

 // reuse the compiler's name mangling to compute native symbol names
@ -656,22 +657,13 @@ class interpreter {

    /** \brief Retrieve Lean declaration from environment. */
    decl get_decl(name const & fn) {
-        option_ref<decl> d = find_env_decl(m_env, fn);
+        option_ref<decl> d = find_ir_decl(m_env, fn);
        if (!d) {
            throw exception(sstream() << "unknown declaration '" << fn << "'");
        }
        return d.get().value();
    }

-    /** \brief Retrieve Lean definition from environment. */
-    decl get_fdecl(name const & fn) {
-        decl d = get_decl(fn);
-        if (decl_tag(d) == decl_kind::Extern) {
-            throw exception(sstream() << "unexpected external declaration '" << fn << "'");
-        }
-        return d;
-    }
-
    /** \brief Evaluate nullary function ("constant"). */
    value load(name const & fn, type t) {
        constant_cache_entry const * cached = m_constant_cache.find(fn);
@ -825,34 +817,32 @@ public:
        g_interpreter = nullptr;
    }

-    object * call_boxed(name const & fn, object ** args) {
+    /** A variant of `call` designed for external uses.
+     *  * takes (owned) `object *`s instead of `arg`s.
+     *  * supports over-application (but no under-application ATM). */
+    object * call_boxed(name const & fn, unsigned n, object ** args) {
        symbol_cache_entry e = lookup_symbol(fn);
-        unsigned n = decl_params(e.m_decl).size();
+        unsigned arity = decl_params(e.m_decl).size();
        object * r;
        if (e.m_addr) {
            push_frame(e.m_decl, 0);
            // directly call boxed function, nothing more to do
            r = curry(e.m_addr, n, args);
        } else {
-            // equivalent code to boxed stubs generated by the compiler: unbox args, box result, decrement borrowed args
-
-            if (decl_tag(e.m_decl) == decl_kind::Extern) {
-                throw exception(sstream() << "unexpected external declaration '" << fn << "'");
+            decl d = e.m_decl;
+            if (option_ref<decl> d_boxed = find_ir_decl(m_env, fn + *g_boxed_suffix)) {
+                d = *d_boxed.get();
            }
+            // `d` now has a boxed signature
            // evaluate args in old stack frame
-            for (unsigned i = 0; i < n; i++) {
-                type t = param_type(decl_params(e.m_decl)[i]);
-                m_arg_stack.push_back(unbox_t(args[i], t));
-                if (type_is_scalar(t)) {
-                    dec(args[i]);
-                }
+            for (unsigned i = 0; i < arity; i++) {
+                m_arg_stack.push_back(args[i]);
            }
            push_frame(e.m_decl, 0);
-            r = box_t(eval_body(decl_fun_body(e.m_decl)), decl_type(e.m_decl));
-            for (size_t i = 0; i < n; i++) {
-                if (param_borrow(decl_params(e.m_decl)[i])) {
-                    dec(args[i]);
-                }
+            r = eval_body(decl_fun_body(e.m_decl)).m_obj;
+            if (n > arity) {
+                // `fn` returned a closure
+                r = apply_n(r, n - arity, &args[arity]);
            }
        }
        pop_frame(r, decl_type(e.m_decl));
@ -860,8 +850,9 @@ public:
    }

    uint32 run_main(int argc, char * argv[]) {
-        decl d = get_fdecl("main");
+        decl d = get_decl("main");
        array_ref<param> const & params = decl_params(d);
+        buffer<object *> args;
        if (params.size() == 2) { // List String -> IO UInt32
            lean_object * in = lean_box(0);
            int i = argc;
@ -872,15 +863,13 @@ public:
                lean_ctor_set(n, 1, in);
                in = n;
            }
-            m_arg_stack.push_back(in);
+            args.push_back(in);
        } else { // IO UInt32
            lean_assert(params.size() == 1);
        }
        object * w = io_mk_world();
-        m_arg_stack.push_back(w);
-        push_frame(d, 0);
-        w = eval_body(decl_fun_body(d)).m_obj;
-        pop_frame(w, type::Object);
+        args.push_back(w);
+        w = call_boxed("main", args.size(), &args[0]);
        if (io_result_is_ok(w)) {
            // NOTE: in an awesome hack, `IO Unit` works just as well because `pure 0` and `pure ()` use the same
            // representation
@ -895,8 +884,8 @@ public:
    }
 };

-object * run_boxed(environment const & env, name const & fn, object ** args) {
-    return interpreter(env).call_boxed(fn, args);
+object * run_boxed(environment const & env, name const & fn, unsigned n, object **args) {
+    return interpreter(env).call_boxed(fn, n, args);
 }
 uint32 run_main(environment const & env, int argv, char * argc[]) {
    return interpreter(env).run_main(argv, argc);
@ -905,6 +894,7 @@ uint32 run_main(environment const & env, int argv, char * argc[]) {

 void initialize_ir_interpreter() {
    ir::g_mangle_prefix = new string_ref("l_");
+    ir::g_boxed_suffix = new string_ref("_boxed");
    ir::g_boxed_mangled_suffix = new string_ref("___boxed");
    DEBUG_CODE({
        register_trace_class({"interpreter"});
@ -915,6 +905,7 @@ void initialize_ir_interpreter() {

 void finalize_ir_interpreter() {
    delete ir::g_boxed_mangled_suffix;
+    delete ir::g_boxed_suffix;
    delete ir::g_mangle_prefix;
 }
 }
--- a/stage0/src/library/compiler/ir_interpreter.h
+++ b/stage0/src/library/compiler/ir_interpreter.h
@ -11,7 +11,7 @@ Author: Sebastian Ullrich
 namespace lean {
 namespace ir {
 /** \brief Run `n` using the "boxed" ABI, i.e. with all-owned parameters. */
-object * run_boxed(environment const & env, name const & fn, object ** args);
+object * run_boxed(environment const & env, name const & fn, unsigned n, object **args);
 uint32 run_main(environment const & env, int argv, char * argc[]);
 }
 void initialize_ir_interpreter();
--- a/stage0/src/util/format.cpp
+++ b/stage0/src/util/format.cpp
@ -110,9 +110,6 @@ void initialize_format() {
    g_pp_indent  = new name{"pp", "indent"};
    g_pp_unicode = new name{"pp", "unicode"};
    g_pp_width   = new name{"pp", "width"};
-    register_unsigned_option(*g_pp_indent, LEAN_DEFAULT_PP_INDENTATION, "(pretty printer) default indentation");
-    register_bool_option(*g_pp_unicode, LEAN_DEFAULT_PP_UNICODE, "(pretty printer) use unicode characters");
-    register_unsigned_option(*g_pp_width, LEAN_DEFAULT_PP_WIDTH, "(pretty printer) line width");
    g_line  = new format(box(static_cast<unsigned>(format::format_kind::LINE)));
    g_space = new format(" ");
 }
--- a/stage0/src/util/init_module.cpp
+++ b/stage0/src/util/init_module.cpp
@ -10,7 +10,6 @@ Author: Leonardo de Moura
 #include "util/fresh_name.h"
 #include "util/name_generator.h"
 #include "util/options.h"
-#include "util/option_declarations.h"
 #include "util/format.h"

 namespace lean {
@ -20,14 +19,12 @@ void initialize_util_module() {
    initialize_name();
    initialize_name_generator();
    initialize_fresh_name();
-    initialize_option_declarations();
    initialize_options();
    initialize_format();
 }
 void finalize_util_module() {
    finalize_format();
    finalize_options();
-    finalize_option_declarations();
    finalize_fresh_name();
    finalize_name_generator();
    finalize_name();
--- a/stage0/src/util/option_declarations.cpp
+++ b/stage0/src/util/option_declarations.cpp
@ -5,69 +5,51 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/option_declarations.h"
+#include "util/array_ref.h"
+#include "util/pair_ref.h"
+#include "util/io.h"

 namespace lean {
-void option_declaration::display_value(std::ostream & out, options const & o) const {
-    bool contains = false;
-    if (o.contains(get_name())) {
-/*
-        sexpr s = o.get_sexpr(get_name());
-        switch (kind()) {
-        case BoolOption:
-            if (!is_nil(s) && is_bool(s)) {
-                out << (to_bool(s) ? "true" : "false");
-                contains = true;
-            }
-            break;
-        case IntOption:
-            if (!is_nil(s) && is_int(s)) {
-                out << to_int(s);
-                contains = true;
-            }
-            break;
-        case UnsignedOption:
-            if (!is_nil(s) && is_int(s)) {
-                out << static_cast<unsigned>(to_int(s));
-                contains = true;
-            }
-            break;
-        case StringOption:
-            if (!is_nil(s) && is_string(s)) {
-                out << to_string(s);
-                contains = true;
-            }
-            break;
-        }
-*/
-    }
-    if (!contains)
-        out << get_default_value();
-}
+typedef object_ref option_decl;

-static option_declarations * g_option_declarations = nullptr;
-static mutex *               g_option_declarations_guard = nullptr;
+extern "C" object * lean_data_value_to_string (obj_arg d);

-void initialize_option_declarations() {
-    g_option_declarations       = new option_declarations();
-    g_option_declarations_guard = new mutex();
-}
-
-void finalize_option_declarations() {
-    delete g_option_declarations;
-    delete g_option_declarations_guard;
-}
+extern "C" object * lean_get_option_decls_array(obj_arg w);

 option_declarations get_option_declarations() {
+    auto decl_array = get_io_result<array_ref<pair_ref<name, option_decl> > > (lean_get_option_decls_array(io_mk_world()));
    option_declarations r;
-    {
-        unique_lock<mutex> lock(*g_option_declarations_guard);
-        r = *g_option_declarations;
+    for (pair_ref<name, option_decl> const & p : decl_array) {
+        option_decl decl = p.snd();
+        data_value def_val = cnstr_get_ref_t<data_value>(decl, 0);
+        string_ref def_str(lean_data_value_to_string(def_val.to_obj_arg()));
+        string_ref descr = cnstr_get_ref_t<string_ref>(decl, 2);
+        data_value_kind kind = static_cast<data_value_kind>(lean_obj_tag(def_val.raw()));
+        option_declaration d(p.fst(), kind, def_str.data(), descr.data());
+        r.insert(p.fst(), d);
    }
    return r;
 }

+data_value mk_data_value(data_value_kind k, char const * val) {
+    switch (k) {
+    case data_value_kind::String:
+        return data_value(val);
+    case data_value_kind::Bool:
+        return strcmp(val, "true") == 0 ? data_value(true) : data_value(false);
+    case data_value_kind::Nat:
+        return data_value(atoi(val));
+    case data_value_kind::Name:
+        return data_value(name(val));
+    default:
+        lean_unreachable();
+    }
+}
+
+extern "C" object * lean_register_option(obj_arg name, obj_arg decl, obj_arg w);
+
 void register_option(name const & n, data_value_kind k, char const * default_value, char const * description) {
-    unique_lock<mutex> lock(*g_option_declarations_guard);
-    g_option_declarations->insert(n, option_declaration(n, k, default_value, description));
+    object_ref decl = mk_cnstr(0, mk_data_value(k, default_value), string_ref(""), string_ref(description));
+    consume_io_result(lean_register_option(n.to_obj_arg(), decl.to_obj_arg(), io_mk_world()));
 }
 }
--- a/stage0/src/util/option_declarations.h
+++ b/stage0/src/util/option_declarations.h
@ -35,8 +35,6 @@ public:
 };

 typedef name_map<option_declaration> option_declarations;
-void initialize_option_declarations();
-void finalize_option_declarations();
 option_declarations get_option_declarations();
 void register_option(name const & n, data_value_kind k, char const * default_value, char const * description);
 #define register_bool_option(n, v, d) register_option(n, data_value_kind::Bool, LEAN_STR(v), d)
--- a/stage0/src/util/options.cpp
+++ b/stage0/src/util/options.cpp
@ -23,9 +23,6 @@ void initialize_options() {
    g_verbose    = new name("verbose");
    g_max_memory = new name("max_memory");
    g_timeout    = new name("timeout");
-    register_bool_option(*g_verbose, LEAN_DEFAULT_VERBOSE, "disable/enable verbose messages");
-    register_unsigned_option(*g_max_memory, LEAN_DEFAULT_MAX_MEMORY, "maximum amount of memory available for Lean in megabytes");
-    register_unsigned_option(*g_timeout, 0, "the (deterministic) timeout is measured as the maximum of memory allocations (in thousands) per task, the default is unbounded");
 }

 void finalize_options() {
--- a/stage0/stdlib/CMakeLists.txt
+++ b/stage0/stdlib/CMakeLists.txt
@ -1 +1 @@
-add_library (stage0 OBJECT Init/./Coe.c Init/./Control.c Init/./Control/Alternative.c Init/./Control/Applicative.c Init/./Control/Conditional.c Init/./Control/EState.c Init/./Control/Except.c Init/./Control/Functor.c Init/./Control/Id.c Init/./Control/Lift.c Init/./Control/Monad.c Init/./Control/MonadFail.c Init/./Control/Option.c Init/./Control/Reader.c Init/./Control/State.c Init/./Core.c Init/./Data.c Init/./Data/Array.c Init/./Data/Array/Basic.c Init/./Data/Array/BinSearch.c Init/./Data/Array/QSort.c Init/./Data/AssocList.c Init/./Data/Basic.c Init/./Data/BinomialHeap.c Init/./Data/BinomialHeap/Basic.c Init/./Data/ByteArray.c Init/./Data/ByteArray/Basic.c Init/./Data/Char.c Init/./Data/Char/Basic.c Init/./Data/DList.c Init/./Data/Fin.c Init/./Data/Fin/Basic.c Init/./Data/HashMap.c Init/./Data/HashMap/Basic.c Init/./Data/HashSet.c Init/./Data/Hashable.c Init/./Data/Int.c Init/./Data/Int/Basic.c Init/./Data/List.c Init/./Data/List/Basic.c Init/./Data/List/BasicAux.c Init/./Data/List/Control.c Init/./Data/List/Instances.c Init/./Data/Nat.c Init/./Data/Nat/Basic.c Init/./Data/Nat/Bitwise.c Init/./Data/Nat/Control.c Init/./Data/Nat/Div.c Init/./Data/Option.c Init/./Data/Option/Basic.c Init/./Data/Option/BasicAux.c Init/./Data/Option/Instances.c Init/./Data/PersistentArray.c Init/./Data/PersistentArray/Basic.c Init/./Data/PersistentHashMap.c Init/./Data/PersistentHashMap/Basic.c Init/./Data/PersistentHashSet.c Init/./Data/Queue.c Init/./Data/Queue/Basic.c Init/./Data/RBMap.c Init/./Data/RBMap/Basic.c Init/./Data/RBMap/BasicAux.c Init/./Data/RBTree.c Init/./Data/RBTree/Basic.c Init/./Data/Random.c Init/./Data/Repr.c Init/./Data/Stack.c Init/./Data/Stack/Basic.c Init/./Data/String.c Init/./Data/String/Basic.c Init/./Data/ToString.c Init/./Data/UInt.c Init/./Default.c Init/./Fix.c Init/./Lean.c Init/./Lean/Attributes.c Init/./Lean/AuxRecursor.c Init/./Lean/Class.c Init/./Lean/Compiler.c Init/./Lean/Compiler/ClosedTermCache.c Init/./Lean/Compiler/ConstFolding.c Init/./Lean/Compiler/ExportAttr.c Init/./Lean/Compiler/ExternAttr.c Init/./Lean/Compiler/IR.c Init/./Lean/Compiler/IR/Basic.c Init/./Lean/Compiler/IR/Borrow.c Init/./Lean/Compiler/IR/Boxing.c Init/./Lean/Compiler/IR/Checker.c Init/./Lean/Compiler/IR/CompilerM.c Init/./Lean/Compiler/IR/CtorLayout.c Init/./Lean/Compiler/IR/ElimDeadBranches.c Init/./Lean/Compiler/IR/ElimDeadVars.c Init/./Lean/Compiler/IR/EmitC.c Init/./Lean/Compiler/IR/EmitUtil.c Init/./Lean/Compiler/IR/ExpandResetReuse.c Init/./Lean/Compiler/IR/Format.c Init/./Lean/Compiler/IR/FreeVars.c Init/./Lean/Compiler/IR/LiveVars.c Init/./Lean/Compiler/IR/NormIds.c Init/./Lean/Compiler/IR/PushProj.c Init/./Lean/Compiler/IR/RC.c Init/./Lean/Compiler/IR/ResetReuse.c Init/./Lean/Compiler/IR/SimpCase.c Init/./Lean/Compiler/IR/UnboxResult.c Init/./Lean/Compiler/ImplementedByAttr.c Init/./Lean/Compiler/InitAttr.c Init/./Lean/Compiler/InlineAttrs.c Init/./Lean/Compiler/NameMangling.c Init/./Lean/Compiler/NeverExtractAttr.c Init/./Lean/Compiler/Specialize.c Init/./Lean/Compiler/Util.c Init/./Lean/Data/Format.c Init/./Lean/Data/KVMap.c Init/./Lean/Data/LBool.c Init/./Lean/Data/LOption.c Init/./Lean/Data/Name.c Init/./Lean/Data/NameGenerator.c Init/./Lean/Data/Options.c Init/./Lean/Data/Position.c Init/./Lean/Data/SMap.c Init/./Lean/Data/Trie.c Init/./Lean/Declaration.c Init/./Lean/Elaborator.c Init/./Lean/Elaborator/Alias.c Init/./Lean/Elaborator/Basic.c Init/./Lean/Elaborator/Command.c Init/./Lean/Elaborator/ElabStrategyAttrs.c Init/./Lean/Elaborator/PreTerm.c Init/./Lean/Elaborator/ResolveName.c Init/./Lean/Elaborator/Term.c Init/./Lean/Environment.c Init/./Lean/EqnCompiler.c Init/./Lean/EqnCompiler/MatchPattern.c Init/./Lean/Expr.c Init/./Lean/Level.c Init/./Lean/Linter.c Init/./Lean/LocalContext.c Init/./Lean/Meta.c Init/./Lean/Meta/AbstractMVars.c Init/./Lean/Meta/AppBuilder.c Init/./Lean/Meta/Basic.c Init/./Lean/Meta/Check.c Init/./Lean/Meta/DiscrTree.c Init/./Lean/Meta/DiscrTreeTypes.c Init/./Lean/Meta/Exception.c Init/./Lean/Meta/ExprDefEq.c Init/./Lean/Meta/FunInfo.c Init/./Lean/Meta/InferType.c Init/./Lean/Meta/Instances.c Init/./Lean/Meta/LevelDefEq.c Init/./Lean/Meta/Offset.c Init/./Lean/Meta/Reduce.c Init/./Lean/Meta/SynthInstance.c Init/./Lean/Meta/WHNF.c Init/./Lean/MetavarContext.c Init/./Lean/Modifiers.c Init/./Lean/Parser.c Init/./Lean/Parser/Command.c Init/./Lean/Parser/Identifier.c Init/./Lean/Parser/Level.c Init/./Lean/Parser/Module.c Init/./Lean/Parser/Parser.c Init/./Lean/Parser/Term.c Init/./Lean/Parser/Transform.c Init/./Lean/ProjFns.c Init/./Lean/ReducibilityAttrs.c Init/./Lean/Runtime.c Init/./Lean/Scopes.c Init/./Lean/Syntax.c Init/./Lean/ToExpr.c Init/./Lean/Util/Message.c Init/./Lean/Util/MonadCache.c Init/./Lean/Util/Path.c Init/./Lean/Util/Profile.c Init/./Lean/Util/Trace.c Init/./Lean/Util/WHNF.c Init/./System.c Init/./System/FilePath.c Init/./System/IO.c Init/./System/Platform.c Init/./Util.c Init/./WF.c)
+add_library (stage0 OBJECT Init/./Coe.c Init/./Control.c Init/./Control/Alternative.c Init/./Control/Applicative.c Init/./Control/Conditional.c Init/./Control/EState.c Init/./Control/Except.c Init/./Control/Functor.c Init/./Control/Id.c Init/./Control/Lift.c Init/./Control/Monad.c Init/./Control/MonadFail.c Init/./Control/Option.c Init/./Control/Reader.c Init/./Control/State.c Init/./Core.c Init/./Data.c Init/./Data/Array.c Init/./Data/Array/Basic.c Init/./Data/Array/BinSearch.c Init/./Data/Array/QSort.c Init/./Data/AssocList.c Init/./Data/Basic.c Init/./Data/BinomialHeap.c Init/./Data/BinomialHeap/Basic.c Init/./Data/ByteArray.c Init/./Data/ByteArray/Basic.c Init/./Data/Char.c Init/./Data/Char/Basic.c Init/./Data/DList.c Init/./Data/Fin.c Init/./Data/Fin/Basic.c Init/./Data/HashMap.c Init/./Data/HashMap/Basic.c Init/./Data/HashSet.c Init/./Data/Hashable.c Init/./Data/Int.c Init/./Data/Int/Basic.c Init/./Data/List.c Init/./Data/List/Basic.c Init/./Data/List/BasicAux.c Init/./Data/List/Control.c Init/./Data/List/Instances.c Init/./Data/Nat.c Init/./Data/Nat/Basic.c Init/./Data/Nat/Bitwise.c Init/./Data/Nat/Control.c Init/./Data/Nat/Div.c Init/./Data/Option.c Init/./Data/Option/Basic.c Init/./Data/Option/BasicAux.c Init/./Data/Option/Instances.c Init/./Data/PersistentArray.c Init/./Data/PersistentArray/Basic.c Init/./Data/PersistentHashMap.c Init/./Data/PersistentHashMap/Basic.c Init/./Data/PersistentHashSet.c Init/./Data/Queue.c Init/./Data/Queue/Basic.c Init/./Data/RBMap.c Init/./Data/RBMap/Basic.c Init/./Data/RBMap/BasicAux.c Init/./Data/RBTree.c Init/./Data/RBTree/Basic.c Init/./Data/Random.c Init/./Data/Repr.c Init/./Data/Stack.c Init/./Data/Stack/Basic.c Init/./Data/String.c Init/./Data/String/Basic.c Init/./Data/ToString.c Init/./Data/UInt.c Init/./Default.c Init/./Fix.c Init/./Lean.c Init/./Lean/Attributes.c Init/./Lean/AuxRecursor.c Init/./Lean/Class.c Init/./Lean/Compiler.c Init/./Lean/Compiler/ClosedTermCache.c Init/./Lean/Compiler/ConstFolding.c Init/./Lean/Compiler/ExportAttr.c Init/./Lean/Compiler/ExternAttr.c Init/./Lean/Compiler/IR.c Init/./Lean/Compiler/IR/Basic.c Init/./Lean/Compiler/IR/Borrow.c Init/./Lean/Compiler/IR/Boxing.c Init/./Lean/Compiler/IR/Checker.c Init/./Lean/Compiler/IR/CompilerM.c Init/./Lean/Compiler/IR/CtorLayout.c Init/./Lean/Compiler/IR/ElimDeadBranches.c Init/./Lean/Compiler/IR/ElimDeadVars.c Init/./Lean/Compiler/IR/EmitC.c Init/./Lean/Compiler/IR/EmitUtil.c Init/./Lean/Compiler/IR/ExpandResetReuse.c Init/./Lean/Compiler/IR/Format.c Init/./Lean/Compiler/IR/FreeVars.c Init/./Lean/Compiler/IR/LiveVars.c Init/./Lean/Compiler/IR/NormIds.c Init/./Lean/Compiler/IR/PushProj.c Init/./Lean/Compiler/IR/RC.c Init/./Lean/Compiler/IR/ResetReuse.c Init/./Lean/Compiler/IR/SimpCase.c Init/./Lean/Compiler/IR/UnboxResult.c Init/./Lean/Compiler/ImplementedByAttr.c Init/./Lean/Compiler/InitAttr.c Init/./Lean/Compiler/InlineAttrs.c Init/./Lean/Compiler/NameMangling.c Init/./Lean/Compiler/NeverExtractAttr.c Init/./Lean/Compiler/Specialize.c Init/./Lean/Compiler/Util.c Init/./Lean/Data/Format.c Init/./Lean/Data/KVMap.c Init/./Lean/Data/LBool.c Init/./Lean/Data/LOption.c Init/./Lean/Data/Name.c Init/./Lean/Data/NameGenerator.c Init/./Lean/Data/Options.c Init/./Lean/Data/Position.c Init/./Lean/Data/SMap.c Init/./Lean/Data/Trie.c Init/./Lean/Declaration.c Init/./Lean/Elaborator.c Init/./Lean/Elaborator/Alias.c Init/./Lean/Elaborator/Basic.c Init/./Lean/Elaborator/Command.c Init/./Lean/Elaborator/ElabStrategyAttrs.c Init/./Lean/Elaborator/PreTerm.c Init/./Lean/Elaborator/ResolveName.c Init/./Lean/Elaborator/Term.c Init/./Lean/Environment.c Init/./Lean/EqnCompiler.c Init/./Lean/EqnCompiler/MatchPattern.c Init/./Lean/Eval.c Init/./Lean/Expr.c Init/./Lean/Level.c Init/./Lean/Linter.c Init/./Lean/LocalContext.c Init/./Lean/Meta.c Init/./Lean/Meta/AbstractMVars.c Init/./Lean/Meta/AppBuilder.c Init/./Lean/Meta/Basic.c Init/./Lean/Meta/Check.c Init/./Lean/Meta/DiscrTree.c Init/./Lean/Meta/DiscrTreeTypes.c Init/./Lean/Meta/Exception.c Init/./Lean/Meta/ExprDefEq.c Init/./Lean/Meta/FunInfo.c Init/./Lean/Meta/InferType.c Init/./Lean/Meta/Instances.c Init/./Lean/Meta/LevelDefEq.c Init/./Lean/Meta/Offset.c Init/./Lean/Meta/Reduce.c Init/./Lean/Meta/SynthInstance.c Init/./Lean/Meta/WHNF.c Init/./Lean/MetavarContext.c Init/./Lean/Modifiers.c Init/./Lean/Parser.c Init/./Lean/Parser/Command.c Init/./Lean/Parser/Identifier.c Init/./Lean/Parser/Level.c Init/./Lean/Parser/Module.c Init/./Lean/Parser/Parser.c Init/./Lean/Parser/Term.c Init/./Lean/Parser/Transform.c Init/./Lean/ProjFns.c Init/./Lean/ReducibilityAttrs.c Init/./Lean/Runtime.c Init/./Lean/Scopes.c Init/./Lean/Syntax.c Init/./Lean/ToExpr.c Init/./Lean/Util/Message.c Init/./Lean/Util/MonadCache.c Init/./Lean/Util/Path.c Init/./Lean/Util/Profile.c Init/./Lean/Util/Trace.c Init/./Lean/Util/WHNF.c Init/./System.c Init/./System/FilePath.c Init/./System/IO.c Init/./System/Platform.c Init/./Util.c Init/./WF.c)
--- a/stage0/stdlib/Init/Lean.c
+++ b/stage0/stdlib/Init/Lean.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean
-// Imports: Init.Lean.Compiler Init.Lean.Environment Init.Lean.Modifiers Init.Lean.ProjFns Init.Lean.Runtime Init.Lean.Attributes Init.Lean.Parser Init.Lean.ReducibilityAttrs Init.Lean.Elaborator Init.Lean.EqnCompiler Init.Lean.Class Init.Lean.LocalContext Init.Lean.MetavarContext Init.Lean.AuxRecursor Init.Lean.Linter Init.Lean.Meta
+// Imports: Init.Lean.Compiler Init.Lean.Environment Init.Lean.Modifiers Init.Lean.ProjFns Init.Lean.Runtime Init.Lean.Attributes Init.Lean.Parser Init.Lean.ReducibilityAttrs Init.Lean.Elaborator Init.Lean.EqnCompiler Init.Lean.Class Init.Lean.LocalContext Init.Lean.MetavarContext Init.Lean.AuxRecursor Init.Lean.Linter Init.Lean.Meta Init.Lean.Eval
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -29,6 +29,7 @@ lean_object* initialize_Init_Lean_MetavarContext(lean_object*);
 lean_object* initialize_Init_Lean_AuxRecursor(lean_object*);
 lean_object* initialize_Init_Lean_Linter(lean_object*);
 lean_object* initialize_Init_Lean_Meta(lean_object*);
+lean_object* initialize_Init_Lean_Eval(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean(lean_object* w) {
 lean_object * res;
@ -82,6 +83,9 @@ lean_dec_ref(res);
 res = initialize_Init_Lean_Meta(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Eval(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus
--- a/stage0/stdlib/Init/Lean/Data/Format.c
+++ b/stage0/stdlib/Init/Lean/Data/Format.c
@ -181,7 +181,7 @@ lean_object* l_Lean_optionHasFormat___rarg(lean_object*);
 lean_object* l_Lean_Format_paren___closed__2;
 lean_object* l_Lean_Format_spaceUptoLine_x27___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Format_getIndent(lean_object*);
-lean_object* l_Lean_registerOption(lean_object*, lean_object*, lean_object*);
+lean_object* lean_register_option(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_HasRepr;
 lean_object* l_Lean_natHasFormat(lean_object*);
 lean_object* lean_format_group(lean_object*);
@ -1572,7 +1572,7 @@ _start:
 lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_2 = l_Lean_Format_getIndent___closed__2;
 x_3 = l_Lean_Format_indentOption___closed__3;
-x_4 = l_Lean_registerOption(x_2, x_3, x_1);
+x_4 = lean_register_option(x_2, x_3, x_1);
 return x_4;
 }
 }
@ -1614,7 +1614,7 @@ _start:
 lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_2 = l_Lean_Format_getUnicode___closed__2;
 x_3 = l_Lean_Format_unicodeOption___closed__3;
-x_4 = l_Lean_registerOption(x_2, x_3, x_1);
+x_4 = lean_register_option(x_2, x_3, x_1);
 return x_4;
 }
 }
@ -1656,7 +1656,7 @@ _start:
 lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_2 = l_Lean_Format_getWidth___closed__4;
 x_3 = l_Lean_Format_widthOption___closed__3;
-x_4 = l_Lean_registerOption(x_2, x_3, x_1);
+x_4 = lean_register_option(x_2, x_3, x_1);
 return x_4;
 }
 }
--- a/stage0/stdlib/Init/Lean/Data/KVMap.c
+++ b/stage0/stdlib/Init/Lean/Data/KVMap.c
@ -13,10 +13,12 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+extern lean_object* l_Lean_Name_toString___closed__1;
 lean_object* l_Lean_KVMap_setBool(lean_object*, lean_object*, uint8_t);
 lean_object* l_Lean_KVMap_insert(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_findCore___main___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_getInt___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_DataValue_hasToString;
 lean_object* l_Lean_KVMap_boolVal___closed__2;
 lean_object* l_Lean_KVMap_natVal___closed__1;
 lean_object* l_Lean_KVMap_stringVal___closed__1;
@ -42,6 +44,7 @@ lean_object* l_Lean_KVMap_stringVal___closed__3;
 lean_object* l_Lean_KVMap_find(lean_object*, lean_object*);
 extern lean_object* l_Int_zero;
 lean_object* l_Lean_KVMap_subsetAux___main___boxed(lean_object*, lean_object*);
+lean_object* l_Int_repr(lean_object*);
 lean_object* l_Lean_nat2DataValue(lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 uint8_t l_Lean_DataValue_beq(lean_object*, lean_object*);
@ -55,6 +58,7 @@ lean_object* l_Lean_KVMap_stringVal___closed__2;
 lean_object* l_Lean_KVMap_intVal___closed__3;
 lean_object* l_Lean_KVMap_getName___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_getString(lean_object*, lean_object*, lean_object*);
+lean_object* l_Nat_repr(lean_object*);
 lean_object* l_Lean_KVMap_getName(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_isEmpty___boxed(lean_object*);
 uint8_t l_Lean_KVMap_subset(lean_object*, lean_object*);
@ -70,6 +74,7 @@ lean_object* l_Lean_KVMap_HasBeq___closed__1;
 uint8_t l_Lean_KVMap_isEmpty(lean_object*);
 lean_object* l_Lean_KVMap_getNat(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_setName(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Bool_HasRepr___closed__1;
 lean_object* l_Lean_string2DataValue(lean_object*);
 lean_object* l_Lean_KVMap_setBool___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_subset___boxed(lean_object*, lean_object*);
@ -77,6 +82,8 @@ lean_object* l_Lean_KVMap_HasBeq;
 lean_object* l_Lean_DataValue_HasBeq;
 lean_object* l_Lean_KVMap_get(lean_object*);
 lean_object* l_Lean_KVMap_empty;
+extern lean_object* l_Bool_HasRepr___closed__2;
+lean_object* lean_data_value_to_string(lean_object*);
 lean_object* l_Lean_KVMap_insertCore(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_boolVal;
 lean_object* l_Lean_KVMap_findCore(lean_object*, lean_object*);
@ -88,9 +95,11 @@ lean_object* l_Lean_KVMap_natVal___closed__2;
 uint8_t l_Lean_KVMap_subsetAux(lean_object*, lean_object*);
 uint8_t l_Lean_KVMap_eqv(lean_object*, lean_object*);
 uint8_t l_List_isEmpty___rarg(lean_object*);
+lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
 lean_object* l_Lean_int2DataValue(lean_object*);
 lean_object* l_Lean_KVMap_natVal;
 lean_object* l_Lean_KVMap_subsetAux___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_DataValue_hasToString___closed__1;
 uint8_t lean_string_dec_eq(lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_getNat___boxed(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_DataValue_beq(lean_object* x_1, lean_object* x_2) {
@ -214,6 +223,84 @@ x_1 = l_Lean_DataValue_HasBeq___closed__1;
 return x_1;
 }
 }
+lean_object* lean_data_value_to_string(lean_object* x_1) {
+_start:
+{
+switch (lean_obj_tag(x_1)) {
+case 0:
+{
+lean_object* x_2; 
+x_2 = lean_ctor_get(x_1, 0);
+lean_inc(x_2);
+lean_dec(x_1);
+return x_2;
+}
+case 1:
+{
+uint8_t x_3; 
+x_3 = lean_ctor_get_uint8(x_1, 0);
+lean_dec(x_1);
+if (x_3 == 0)
+{
+lean_object* x_4; 
+x_4 = l_Bool_HasRepr___closed__1;
+return x_4;
+}
+else
+{
+lean_object* x_5; 
+x_5 = l_Bool_HasRepr___closed__2;
+return x_5;
+}
+}
+case 2:
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; 
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = l_Lean_Name_toString___closed__1;
+x_8 = l_Lean_Name_toStringWithSep___main(x_7, x_6);
+return x_8;
+}
+case 3:
+{
+lean_object* x_9; lean_object* x_10; 
+x_9 = lean_ctor_get(x_1, 0);
+lean_inc(x_9);
+lean_dec(x_1);
+x_10 = l_Nat_repr(x_9);
+return x_10;
+}
+default: 
+{
+lean_object* x_11; lean_object* x_12; 
+x_11 = lean_ctor_get(x_1, 0);
+lean_inc(x_11);
+lean_dec(x_1);
+x_12 = l_Int_repr(x_11);
+lean_dec(x_11);
+return x_12;
+}
+}
+}
+}
+lean_object* _init_l_Lean_DataValue_hasToString___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(lean_data_value_to_string), 1, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Lean_DataValue_hasToString() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_DataValue_hasToString___closed__1;
+return x_1;
+}
+}
 lean_object* l_Lean_string2DataValue(lean_object* x_1) {
 _start:
 {
@ -1213,6 +1300,10 @@ l_Lean_DataValue_HasBeq___closed__1 = _init_l_Lean_DataValue_HasBeq___closed__1(
 lean_mark_persistent(l_Lean_DataValue_HasBeq___closed__1);
 l_Lean_DataValue_HasBeq = _init_l_Lean_DataValue_HasBeq();
 lean_mark_persistent(l_Lean_DataValue_HasBeq);
+l_Lean_DataValue_hasToString___closed__1 = _init_l_Lean_DataValue_hasToString___closed__1();
+lean_mark_persistent(l_Lean_DataValue_hasToString___closed__1);
+l_Lean_DataValue_hasToString = _init_l_Lean_DataValue_hasToString();
+lean_mark_persistent(l_Lean_DataValue_hasToString);
 l_Lean_KVMap_empty = _init_l_Lean_KVMap_empty();
 lean_mark_persistent(l_Lean_KVMap_empty);
 l_Lean_KVMap_HasBeq___closed__1 = _init_l_Lean_KVMap_HasBeq___closed__1();
--- a/stage0/stdlib/Init/Lean/Data/Options.c
+++ b/stage0/stdlib/Init/Lean/Data/Options.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Data.Options
-// Imports: Init.System.IO Init.Data.ToString Init.Lean.Data.KVMap
+// Imports: Init.System.IO Init.Data.Array Init.Data.ToString Init.Lean.Data.KVMap
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -19,16 +19,22 @@ lean_object* l_Lean_KVMap_setBool(lean_object*, lean_object*, uint8_t);
 lean_object* l_RBNode_find___main___at_Lean_getOptionDecl___spec__1(lean_object*, lean_object*);
 uint8_t l_Lean_Name_quickLt(lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_setNat(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Array_empty___closed__1;
+lean_object* l_Lean_verboseOption___closed__3;
 lean_object* l_String_toNat(lean_object*);
 lean_object* lean_io_mk_ref(lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_setString(lean_object*, lean_object*, lean_object*);
 lean_object* lean_io_ref_get(lean_object*, lean_object*);
+lean_object* l_Lean_maxMemoryOption(lean_object*);
 lean_object* l_Lean_getOptionDefaulValue(lean_object*, lean_object*);
 lean_object* l_Lean_getOptionDecls(lean_object*);
+lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
+extern lean_object* l_String_splitAux___main___closed__1;
 lean_object* l_String_splitOn(lean_object*, lean_object*);
 lean_object* l_Lean_getOptionDecl___closed__1;
 uint8_t l_Lean_NameMap_contains___rarg(lean_object*, lean_object*);
+lean_object* l_Lean_timeoutOption___closed__4;
 lean_object* l_Lean_registerOption___closed__1;
 lean_object* l_Lean_registerOption___closed__2;
 lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
@ -37,29 +43,47 @@ lean_object* l_Lean_setOptionFromString___closed__4;
 lean_object* l_Lean_getOptionDecl(lean_object*, lean_object*);
 lean_object* l_RBNode_find___main___at_Lean_getOptionDecl___spec__1___boxed(lean_object*, lean_object*);
 extern lean_object* l_Char_HasRepr___closed__1;
+lean_object* lean_get_option_decls_array(lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_setInt(lean_object*, lean_object*, lean_object*);
 uint8_t l_String_isNat(lean_object*);
+lean_object* l_Lean_verboseOption___closed__4;
 lean_object* l_Lean_Options_empty;
 lean_object* l_Lean_setOptionFromString___closed__5;
+lean_object* l_Lean_maxMemoryOption___closed__5;
+lean_object* l_Lean_maxMemoryOption___closed__3;
 lean_object* l_Lean_KVMap_setName(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Bool_HasRepr___closed__1;
+lean_object* l_Lean_timeoutOption___closed__2;
 lean_object* l_Lean_setOptionFromString(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Bool_HasRepr___closed__2;
 lean_object* l___private_Init_Lean_Data_Options_1__initOptionDeclsRef(lean_object*);
+lean_object* l_Lean_verboseOption___closed__2;
 lean_object* l_Lean_setOptionFromString___closed__1;
-lean_object* l_Lean_registerOption(lean_object*, lean_object*, lean_object*);
+lean_object* lean_register_option(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_verboseOption___closed__1;
+lean_object* l_Lean_timeoutOption___closed__1;
+lean_object* l_Lean_maxMemoryOption___closed__1;
 lean_object* lean_io_ref_set(lean_object*, lean_object*, lean_object*);
+lean_object* l_RBNode_fold___main___at_Lean_getOptionDeclsArray___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_String_trim(lean_object*);
+lean_object* l_Lean_maxMemoryOption___closed__2;
 lean_object* l_String_toInt(lean_object*);
 lean_object* l_Lean_setOptionFromString___closed__2;
+lean_object* l_Lean_timeoutOption___closed__3;
 lean_object* l_Lean_Options_HasEmptyc;
+lean_object* l_RBNode_fold___main___at_Lean_getOptionDeclsArray___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
+lean_object* l_Lean_verboseOption___closed__5;
 lean_object* l_Lean_getOptionDescr(lean_object*, lean_object*);
+lean_object* l_Lean_timeoutOption(lean_object*);
 lean_object* l_Lean_setOptionFromString___closed__3;
+lean_object* l_Lean_maxMemoryOption___closed__4;
 lean_object* l___private_Init_Lean_Data_Options_2__optionDeclsRef;
 lean_object* l_List_map___main___at_Lean_setOptionFromString___spec__1(lean_object*);
 uint8_t lean_string_dec_eq(lean_object*, lean_object*);
+lean_object* l_Lean_verboseOption(lean_object*);
+lean_object* l_Lean_timeoutOption___closed__5;
 lean_object* _init_l_Lean_Options_empty() {
 _start:
 {
@ -101,7 +125,7 @@ x_1 = lean_mk_string("', option already exists");
 return x_1;
 }
 }
-lean_object* l_Lean_registerOption(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* lean_register_option(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; lean_object* x_5; 
@ -212,6 +236,103 @@ x_3 = lean_io_ref_get(x_2, x_1);
 return x_3;
 }
 }
+lean_object* l_RBNode_fold___main___at_Lean_getOptionDeclsArray___spec__1(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+if (lean_obj_tag(x_2) == 0)
+{
+return x_1;
+}
+else
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_3 = lean_ctor_get(x_2, 0);
+x_4 = lean_ctor_get(x_2, 1);
+x_5 = lean_ctor_get(x_2, 2);
+x_6 = lean_ctor_get(x_2, 3);
+x_7 = l_RBNode_fold___main___at_Lean_getOptionDeclsArray___spec__1(x_1, x_3);
+lean_inc(x_5);
+lean_inc(x_4);
+x_8 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_8, 0, x_4);
+lean_ctor_set(x_8, 1, x_5);
+x_9 = lean_array_push(x_7, x_8);
+x_1 = x_9;
+x_2 = x_6;
+goto _start;
+}
+}
+}
+lean_object* lean_get_option_decls_array(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; 
+x_2 = l___private_Init_Lean_Data_Options_2__optionDeclsRef;
+x_3 = lean_io_ref_get(x_2, x_1);
+if (lean_obj_tag(x_3) == 0)
+{
+uint8_t x_4; 
+x_4 = !lean_is_exclusive(x_3);
+if (x_4 == 0)
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_5 = lean_ctor_get(x_3, 0);
+x_6 = l_Array_empty___closed__1;
+x_7 = l_RBNode_fold___main___at_Lean_getOptionDeclsArray___spec__1(x_6, x_5);
+lean_dec(x_5);
+lean_ctor_set(x_3, 0, x_7);
+return x_3;
+}
+else
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_8 = lean_ctor_get(x_3, 0);
+x_9 = lean_ctor_get(x_3, 1);
+lean_inc(x_9);
+lean_inc(x_8);
+lean_dec(x_3);
+x_10 = l_Array_empty___closed__1;
+x_11 = l_RBNode_fold___main___at_Lean_getOptionDeclsArray___spec__1(x_10, x_8);
+lean_dec(x_8);
+x_12 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_12, 0, x_11);
+lean_ctor_set(x_12, 1, x_9);
+return x_12;
+}
+}
+else
+{
+uint8_t x_13; 
+x_13 = !lean_is_exclusive(x_3);
+if (x_13 == 0)
+{
+return x_3;
+}
+else
+{
+lean_object* x_14; lean_object* x_15; lean_object* x_16; 
+x_14 = lean_ctor_get(x_3, 0);
+x_15 = lean_ctor_get(x_3, 1);
+lean_inc(x_15);
+lean_inc(x_14);
+lean_dec(x_3);
+x_16 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_16, 0, x_14);
+lean_ctor_set(x_16, 1, x_15);
+return x_16;
+}
+}
+}
+}
+lean_object* l_RBNode_fold___main___at_Lean_getOptionDeclsArray___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_RBNode_fold___main___at_Lean_getOptionDeclsArray___spec__1(x_1, x_2);
+lean_dec(x_2);
+return x_3;
+}
+}
 lean_object* l_RBNode_find___main___at_Lean_getOptionDecl___spec__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
@ -1007,7 +1128,188 @@ return x_129;
 }
 }
 }
+lean_object* _init_l_Lean_verboseOption___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("verbose");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_verboseOption___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_verboseOption___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_verboseOption___closed__3() {
+_start:
+{
+uint8_t x_1; lean_object* x_2; 
+x_1 = 1;
+x_2 = lean_alloc_ctor(1, 0, 1);
+lean_ctor_set_uint8(x_2, 0, x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_verboseOption___closed__4() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("disable/enable verbose messages");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_verboseOption___closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_verboseOption___closed__3;
+x_2 = l_String_splitAux___main___closed__1;
+x_3 = l_Lean_verboseOption___closed__4;
+x_4 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_4, 0, x_1);
+lean_ctor_set(x_4, 1, x_2);
+lean_ctor_set(x_4, 2, x_3);
+return x_4;
+}
+}
+lean_object* l_Lean_verboseOption(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_2 = l_Lean_verboseOption___closed__2;
+x_3 = l_Lean_verboseOption___closed__5;
+x_4 = lean_register_option(x_2, x_3, x_1);
+return x_4;
+}
+}
+lean_object* _init_l_Lean_timeoutOption___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("timeout");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_timeoutOption___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_timeoutOption___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_timeoutOption___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = lean_unsigned_to_nat(0u);
+x_2 = lean_alloc_ctor(3, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_timeoutOption___closed__4() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("the (deterministic) timeout is measured as the maximum of memory allocations (in thousands) per task, the default is unbounded");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_timeoutOption___closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_timeoutOption___closed__3;
+x_2 = l_String_splitAux___main___closed__1;
+x_3 = l_Lean_timeoutOption___closed__4;
+x_4 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_4, 0, x_1);
+lean_ctor_set(x_4, 1, x_2);
+lean_ctor_set(x_4, 2, x_3);
+return x_4;
+}
+}
+lean_object* l_Lean_timeoutOption(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_2 = l_Lean_timeoutOption___closed__2;
+x_3 = l_Lean_timeoutOption___closed__5;
+x_4 = lean_register_option(x_2, x_3, x_1);
+return x_4;
+}
+}
+lean_object* _init_l_Lean_maxMemoryOption___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("maxMemory");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_maxMemoryOption___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_maxMemoryOption___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_maxMemoryOption___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = lean_unsigned_to_nat(2048u);
+x_2 = lean_alloc_ctor(3, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_maxMemoryOption___closed__4() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("maximum amount of memory available for Lean in megabytes");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_maxMemoryOption___closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_maxMemoryOption___closed__3;
+x_2 = l_String_splitAux___main___closed__1;
+x_3 = l_Lean_maxMemoryOption___closed__4;
+x_4 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_4, 0, x_1);
+lean_ctor_set(x_4, 1, x_2);
+lean_ctor_set(x_4, 2, x_3);
+return x_4;
+}
+}
+lean_object* l_Lean_maxMemoryOption(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_2 = l_Lean_maxMemoryOption___closed__2;
+x_3 = l_Lean_maxMemoryOption___closed__5;
+x_4 = lean_register_option(x_2, x_3, x_1);
+return x_4;
+}
+}
 lean_object* initialize_Init_System_IO(lean_object*);
+lean_object* initialize_Init_Data_Array(lean_object*);
 lean_object* initialize_Init_Data_ToString(lean_object*);
 lean_object* initialize_Init_Lean_Data_KVMap(lean_object*);
 static bool _G_initialized = false;
@ -1018,6 +1320,9 @@ _G_initialized = true;
 res = initialize_Init_System_IO(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Data_Array(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 res = initialize_Init_Data_ToString(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
@ -1049,6 +1354,45 @@ l_Lean_setOptionFromString___closed__4 = _init_l_Lean_setOptionFromString___clos
 lean_mark_persistent(l_Lean_setOptionFromString___closed__4);
 l_Lean_setOptionFromString___closed__5 = _init_l_Lean_setOptionFromString___closed__5();
 lean_mark_persistent(l_Lean_setOptionFromString___closed__5);
+l_Lean_verboseOption___closed__1 = _init_l_Lean_verboseOption___closed__1();
+lean_mark_persistent(l_Lean_verboseOption___closed__1);
+l_Lean_verboseOption___closed__2 = _init_l_Lean_verboseOption___closed__2();
+lean_mark_persistent(l_Lean_verboseOption___closed__2);
+l_Lean_verboseOption___closed__3 = _init_l_Lean_verboseOption___closed__3();
+lean_mark_persistent(l_Lean_verboseOption___closed__3);
+l_Lean_verboseOption___closed__4 = _init_l_Lean_verboseOption___closed__4();
+lean_mark_persistent(l_Lean_verboseOption___closed__4);
+l_Lean_verboseOption___closed__5 = _init_l_Lean_verboseOption___closed__5();
+lean_mark_persistent(l_Lean_verboseOption___closed__5);
+res = l_Lean_verboseOption(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_Lean_timeoutOption___closed__1 = _init_l_Lean_timeoutOption___closed__1();
+lean_mark_persistent(l_Lean_timeoutOption___closed__1);
+l_Lean_timeoutOption___closed__2 = _init_l_Lean_timeoutOption___closed__2();
+lean_mark_persistent(l_Lean_timeoutOption___closed__2);
+l_Lean_timeoutOption___closed__3 = _init_l_Lean_timeoutOption___closed__3();
+lean_mark_persistent(l_Lean_timeoutOption___closed__3);
+l_Lean_timeoutOption___closed__4 = _init_l_Lean_timeoutOption___closed__4();
+lean_mark_persistent(l_Lean_timeoutOption___closed__4);
+l_Lean_timeoutOption___closed__5 = _init_l_Lean_timeoutOption___closed__5();
+lean_mark_persistent(l_Lean_timeoutOption___closed__5);
+res = l_Lean_timeoutOption(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_Lean_maxMemoryOption___closed__1 = _init_l_Lean_maxMemoryOption___closed__1();
+lean_mark_persistent(l_Lean_maxMemoryOption___closed__1);
+l_Lean_maxMemoryOption___closed__2 = _init_l_Lean_maxMemoryOption___closed__2();
+lean_mark_persistent(l_Lean_maxMemoryOption___closed__2);
+l_Lean_maxMemoryOption___closed__3 = _init_l_Lean_maxMemoryOption___closed__3();
+lean_mark_persistent(l_Lean_maxMemoryOption___closed__3);
+l_Lean_maxMemoryOption___closed__4 = _init_l_Lean_maxMemoryOption___closed__4();
+lean_mark_persistent(l_Lean_maxMemoryOption___closed__4);
+l_Lean_maxMemoryOption___closed__5 = _init_l_Lean_maxMemoryOption___closed__5();
+lean_mark_persistent(l_Lean_maxMemoryOption___closed__5);
+res = l_Lean_maxMemoryOption(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus
--- a/stage0/stdlib/Init/Lean/Elaborator/Basic.c
+++ b/stage0/stdlib/Init/Lean/Elaborator/Basic.c
@ -121,7 +121,6 @@ lean_object* l_Lean_Elab_inPattern___rarg(lean_object*);
 lean_object* l_Lean_SMap_empty___at_Lean_mkBuiltinTermElabTable___spec__1___closed__1;
 lean_object* l_Lean_Elab_mkAnonymousInstName___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_runElab___at_Lean_Elab_processCommand___spec__1___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* l_IO_println___at_HasRepr_HasEval___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_checkSyntaxNodeKindAtNamespaces___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_commandElabAttribute___closed__1;
 lean_object* l_AssocList_find___main___at_Lean_Elab_elabCommand___spec__6(lean_object*, lean_object*);
@ -203,6 +202,7 @@ lean_object* l_Lean_Elab_runElab___rarg(lean_object*, lean_object*, lean_object*
 lean_object* l_PersistentHashMap_findAux___main___at_Lean_Elab_elabCommand___spec__3___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_ElabScope_Inhabited;
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
+lean_object* l_IO_println___at_Lean_HasRepr_HasEval___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_mkElabAttribute___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_AssocList_contains___main___at_Lean_addBuiltinTermElab___spec__3___boxed(lean_object*, lean_object*);
 lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
@ -10068,7 +10068,7 @@ lean_inc(x_9);
 x_10 = lean_ctor_get(x_8, 1);
 lean_inc(x_10);
 lean_dec(x_8);
-x_11 = l_IO_println___at_HasRepr_HasEval___spec__1(x_9, x_10);
+x_11 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_9, x_10);
 lean_dec(x_9);
 if (lean_obj_tag(x_11) == 0)
 {
--- a/stage0/stdlib/Init/Lean/Elaborator/Command.c
+++ b/stage0/stdlib/Init/Lean/Elaborator/Command.c
@ -165,7 +165,6 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__2;
 lean_object* l_Lean_Elab_elabNotation___rarg(lean_object*);
 extern lean_object* l_Option_HasRepr___rarg___closed__3;
 lean_object* l_IO_println___at___private_Init_Lean_Parser_Module_4__testModuleParserAux___main___spec__1(lean_object*, lean_object*);
-lean_object* l_IO_println___at_HasRepr_HasEval___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabElab___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_drop___main___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabOpen___boxed(lean_object*, lean_object*, lean_object*);
@ -180,6 +179,7 @@ lean_object* l_Lean_Elab_elabExport(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_elabUniverse___closed__3;
 lean_object* l___regBuiltinTermElab_Lean_Elab_elabExport___closed__2;
 extern lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__2;
+lean_object* l_IO_println___at_Lean_HasRepr_HasEval___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_elabVariable___closed__1;
 lean_object* l___private_Init_Lean_Elaborator_Command_3__checkAnonymousScope___boxed(lean_object*);
 lean_object* l___private_Init_Lean_Elaborator_Command_1__addScopes(lean_object*, uint8_t, lean_object*, lean_object*);
@ -3797,7 +3797,7 @@ x_28 = l_String_Iterator_HasRepr___closed__2;
 x_29 = lean_string_append(x_27, x_28);
 x_30 = lean_string_append(x_29, x_16);
 lean_dec(x_16);
-x_31 = lean_alloc_closure((void*)(l_IO_println___at_HasRepr_HasEval___spec__1___boxed), 2, 1);
+x_31 = lean_alloc_closure((void*)(l_IO_println___at_Lean_HasRepr_HasEval___spec__1___boxed), 2, 1);
 lean_closure_set(x_31, 0, x_30);
 x_32 = l_Lean_Elab_runIOUnsafe___rarg(x_31, x_2, x_15);
 if (lean_obj_tag(x_32) == 0)
@ -3938,7 +3938,7 @@ lean_inc(x_14);
 lean_dec(x_12);
 x_15 = lean_expr_dbg_to_string(x_13);
 lean_dec(x_13);
-x_16 = lean_alloc_closure((void*)(l_IO_println___at_HasRepr_HasEval___spec__1___boxed), 2, 1);
+x_16 = lean_alloc_closure((void*)(l_IO_println___at_Lean_HasRepr_HasEval___spec__1___boxed), 2, 1);
 lean_closure_set(x_16, 0, x_15);
 x_17 = l_Lean_Elab_runIOUnsafe___rarg(x_16, x_2, x_14);
 lean_dec(x_2);
@ -4185,7 +4185,7 @@ lean_inc(x_28);
 lean_dec(x_12);
 x_29 = lean_expr_dbg_to_string(x_28);
 lean_dec(x_28);
-x_30 = lean_alloc_closure((void*)(l_IO_println___at_HasRepr_HasEval___spec__1___boxed), 2, 1);
+x_30 = lean_alloc_closure((void*)(l_IO_println___at_Lean_HasRepr_HasEval___spec__1___boxed), 2, 1);
 lean_closure_set(x_30, 0, x_29);
 x_31 = l_Lean_Elab_runIOUnsafe___rarg(x_30, x_2, x_13);
 lean_dec(x_2);
--- a/stage0/stdlib/Init/Lean/Elaborator/PreTerm.c
+++ b/stage0/stdlib/Init/Lean/Elaborator/PreTerm.c
@ -186,7 +186,6 @@ lean_object* l_Lean_Syntax_getNumArgs___rarg(lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_convertType___closed__5;
 lean_object* l_Lean_Elab_toLevel___main___closed__1;
 lean_object* l_Lean_Elab_toLevel___main___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* l_IO_println___at_HasRepr_HasEval___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elaborator_PreTerm_4__processBinder___closed__3;
 extern lean_object* l_Lean_Syntax_formatStx___main___rarg___closed__5;
 lean_object* lean_local_ctx_find_from_user_name(lean_object*, lean_object*);
@ -205,6 +204,7 @@ extern lean_object* l_Lean_Parser_Level_paren___elambda__1___rarg___closed__3;
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 lean_object* l_Lean_mkApp(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__1;
+lean_object* l_IO_println___at_Lean_HasRepr_HasEval___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_mkForall(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_registerTagAttribute___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_panic(lean_object*, lean_object*, lean_object*);
@ -3661,7 +3661,7 @@ x_37 = l_Lean_Format_pretty(x_35, x_36);
 x_38 = l___private_Init_Lean_Elaborator_PreTerm_4__processBinder___closed__3;
 x_39 = lean_string_append(x_38, x_37);
 lean_dec(x_37);
-x_40 = lean_alloc_closure((void*)(l_IO_println___at_HasRepr_HasEval___spec__1___boxed), 2, 1);
+x_40 = lean_alloc_closure((void*)(l_IO_println___at_Lean_HasRepr_HasEval___spec__1___boxed), 2, 1);
 lean_closure_set(x_40, 0, x_39);
 x_41 = l_Lean_Elab_runIOUnsafe___rarg(x_40, x_2, x_3);
 lean_dec(x_2);
@ -3725,7 +3725,7 @@ x_54 = l_Lean_Format_pretty(x_52, x_53);
 x_55 = l___private_Init_Lean_Elaborator_PreTerm_4__processBinder___closed__4;
 x_56 = lean_string_append(x_55, x_54);
 lean_dec(x_54);
-x_57 = lean_alloc_closure((void*)(l_IO_println___at_HasRepr_HasEval___spec__1___boxed), 2, 1);
+x_57 = lean_alloc_closure((void*)(l_IO_println___at_Lean_HasRepr_HasEval___spec__1___boxed), 2, 1);
 lean_closure_set(x_57, 0, x_56);
 x_58 = l_Lean_Elab_runIOUnsafe___rarg(x_57, x_2, x_3);
 lean_dec(x_2);
--- a/stage0/stdlib/Init/Lean/Environment.c
+++ b/stage0/stdlib/Init/Lean/Environment.c
@ -118,7 +118,6 @@ lean_object* l_AssocList_contains___main___at_Lean_Environment_addAux___spec__7_
 uint8_t l_HashMapImp_contains___at_Lean_Environment_contains___spec__2(lean_object*, lean_object*);
 lean_object* l_Lean_namespacesExt___closed__2;
 lean_object* l_Lean_namespacesExt___elambda__3___boxed(lean_object*, lean_object*);
-lean_object* l_IO_println___at_HasRepr_HasEval___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__4(lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_inhabited(lean_object*, lean_object*);
 extern lean_object* l_Lean_LocalContext_Inhabited___closed__1;
@ -184,6 +183,7 @@ lean_object* l_Lean_ModuleData_inhabited___closed__1;
 lean_object* lean_set_extension(lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_foldAux___main___at_Lean_mkModuleData___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
+lean_object* l_IO_println___at_Lean_HasRepr_HasEval___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_SimplePersistentEnvExtension_modifyState___rarg___lambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_SMap_size___at_Lean_Environment_displayStats___spec__3___boxed(lean_object*);
 lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
@ -11292,7 +11292,7 @@ x_16 = lean_string_append(x_15, x_14);
 lean_dec(x_14);
 x_17 = l_Char_HasRepr___closed__1;
 x_18 = lean_string_append(x_16, x_17);
-x_19 = l_IO_println___at_HasRepr_HasEval___spec__1(x_18, x_4);
+x_19 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_18, x_4);
 lean_dec(x_18);
 if (lean_obj_tag(x_19) == 0)
 {
@ -11321,7 +11321,7 @@ x_30 = l_Lean_Format_pretty(x_28, x_29);
 x_31 = l_Array_forMAux___main___at_Lean_Environment_displayStats___spec__9___closed__2;
 x_32 = lean_string_append(x_31, x_30);
 lean_dec(x_30);
-x_33 = l_IO_println___at_HasRepr_HasEval___spec__1(x_32, x_20);
+x_33 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_32, x_20);
 lean_dec(x_32);
 if (lean_obj_tag(x_33) == 0)
 {
@ -11340,7 +11340,7 @@ x_38 = l_Nat_repr(x_37);
 x_39 = l_Array_forMAux___main___at_Lean_Environment_displayStats___spec__9___closed__3;
 x_40 = lean_string_append(x_39, x_38);
 lean_dec(x_38);
-x_41 = l_IO_println___at_HasRepr_HasEval___spec__1(x_40, x_34);
+x_41 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_40, x_34);
 lean_dec(x_40);
 if (lean_obj_tag(x_41) == 0)
 {
@ -11417,7 +11417,7 @@ x_55 = l_Nat_repr(x_54);
 x_56 = l_Array_forMAux___main___at_Lean_Environment_displayStats___spec__9___closed__3;
 x_57 = lean_string_append(x_56, x_55);
 lean_dec(x_55);
-x_58 = l_IO_println___at_HasRepr_HasEval___spec__1(x_57, x_20);
+x_58 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_57, x_20);
 lean_dec(x_57);
 if (lean_obj_tag(x_58) == 0)
 {
@ -11584,7 +11584,7 @@ lean_dec(x_17);
 x_20 = l_Lean_Environment_displayStats___closed__1;
 x_21 = lean_string_append(x_20, x_19);
 lean_dec(x_19);
-x_22 = l_IO_println___at_HasRepr_HasEval___spec__1(x_21, x_6);
+x_22 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_21, x_6);
 lean_dec(x_21);
 if (lean_obj_tag(x_22) == 0)
 {
@ -11596,7 +11596,7 @@ x_24 = l_Nat_repr(x_13);
 x_25 = l_Lean_Environment_displayStats___closed__2;
 x_26 = lean_string_append(x_25, x_24);
 lean_dec(x_24);
-x_27 = l_IO_println___at_HasRepr_HasEval___spec__1(x_26, x_23);
+x_27 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_26, x_23);
 lean_dec(x_26);
 if (lean_obj_tag(x_27) == 0)
 {
@ -11611,7 +11611,7 @@ x_31 = l_Nat_repr(x_30);
 x_32 = l_Lean_Environment_displayStats___closed__3;
 x_33 = lean_string_append(x_32, x_31);
 lean_dec(x_31);
-x_34 = l_IO_println___at_HasRepr_HasEval___spec__1(x_33, x_28);
+x_34 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_33, x_28);
 lean_dec(x_33);
 if (lean_obj_tag(x_34) == 0)
 {
@ -11626,7 +11626,7 @@ x_38 = l_Nat_repr(x_37);
 x_39 = l_Lean_Environment_displayStats___closed__4;
 x_40 = lean_string_append(x_39, x_38);
 lean_dec(x_38);
-x_41 = l_IO_println___at_HasRepr_HasEval___spec__1(x_40, x_35);
+x_41 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_40, x_35);
 lean_dec(x_40);
 if (lean_obj_tag(x_41) == 0)
 {
@ -11641,7 +11641,7 @@ x_44 = l_Nat_repr(x_43);
 x_45 = l_Lean_Environment_displayStats___closed__5;
 x_46 = lean_string_append(x_45, x_44);
 lean_dec(x_44);
-x_47 = l_IO_println___at_HasRepr_HasEval___spec__1(x_46, x_42);
+x_47 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_46, x_42);
 lean_dec(x_46);
 if (lean_obj_tag(x_47) == 0)
 {
@ -11655,7 +11655,7 @@ x_50 = l_Nat_repr(x_49);
 x_51 = l_Lean_Environment_displayStats___closed__6;
 x_52 = lean_string_append(x_51, x_50);
 lean_dec(x_50);
-x_53 = l_IO_println___at_HasRepr_HasEval___spec__1(x_52, x_48);
+x_53 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_52, x_48);
 lean_dec(x_52);
 if (lean_obj_tag(x_53) == 0)
 {
@ -11670,7 +11670,7 @@ x_57 = l_Nat_repr(x_56);
 x_58 = l_Lean_Environment_displayStats___closed__7;
 x_59 = lean_string_append(x_58, x_57);
 lean_dec(x_57);
-x_60 = l_IO_println___at_HasRepr_HasEval___spec__1(x_59, x_54);
+x_60 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_59, x_54);
 lean_dec(x_59);
 if (lean_obj_tag(x_60) == 0)
 {
@ -11686,7 +11686,7 @@ x_64 = l_Nat_repr(x_63);
 x_65 = l_Lean_Environment_displayStats___closed__8;
 x_66 = lean_string_append(x_65, x_64);
 lean_dec(x_64);
-x_67 = l_IO_println___at_HasRepr_HasEval___spec__1(x_66, x_61);
+x_67 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_66, x_61);
 lean_dec(x_66);
 if (lean_obj_tag(x_67) == 0)
 {
--- a/stage0/stdlib/Init/Lean/Eval.c
+++ b/stage0/stdlib/Init/Lean/Eval.c
@ -0,0 +1,62 @@
+// Lean compiler output
+// Module: Init.Lean.Eval
+// Imports: Init.System.IO Init.Lean.Environment
+#include "runtime/lean.h"
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+lean_object* l_Lean_MetaHasEvalOfHasEval(lean_object*);
+lean_object* l_Lean_MetaHasEvalOfHasEval___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_MetaHasEvalOfHasEval___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_MetaHasEvalOfHasEval___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+lean_object* x_6; 
+x_6 = lean_apply_2(x_1, x_4, x_5);
+return x_6;
+}
+}
+lean_object* l_Lean_MetaHasEvalOfHasEval(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_MetaHasEvalOfHasEval___rarg___boxed), 5, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_MetaHasEvalOfHasEval___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+lean_object* x_6; 
+x_6 = l_Lean_MetaHasEvalOfHasEval___rarg(x_1, x_2, x_3, x_4, x_5);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_6;
+}
+}
+lean_object* initialize_Init_System_IO(lean_object*);
+lean_object* initialize_Init_Lean_Environment(lean_object*);
+static bool _G_initialized = false;
+lean_object* initialize_Init_Lean_Eval(lean_object* w) {
+lean_object * res;
+if (_G_initialized) return lean_mk_io_result(lean_box(0));
+_G_initialized = true;
+res = initialize_Init_System_IO(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Init_Lean_Environment(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+return lean_mk_io_result(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif
--- a/stage0/stdlib/Init/Lean/Message.c
+++ b/stage0/stdlib/Init/Lean/Message.c
--- a/stage0/stdlib/Init/Lean/Meta/Basic.c
+++ b/stage0/stdlib/Init/Lean/Meta/Basic.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Meta.Basic
-// Imports: Init.Control.Reader Init.Lean.Data.LOption Init.Lean.Data.NameGenerator Init.Lean.Environment Init.Lean.Class Init.Lean.ReducibilityAttrs Init.Lean.Util.Trace Init.Lean.Meta.Exception Init.Lean.Meta.DiscrTreeTypes
+// Imports: Init.Control.Reader Init.Lean.Data.LOption Init.Lean.Data.NameGenerator Init.Lean.Environment Init.Lean.Class Init.Lean.ReducibilityAttrs Init.Lean.Util.Trace Init.Lean.Meta.Exception Init.Lean.Meta.DiscrTreeTypes Init.Lean.Eval
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -22,6 +22,7 @@ lean_object* l_Lean_Meta_withLocalDecl(lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isClassExpensive___main___spec__5___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkFreshLevelMVar(lean_object*);
 lean_object* l_Lean_Meta_mkFreshId___boxed(lean_object*);
+lean_object* l_PersistentHashMap_empty___at_Lean_Meta_MetaHasEval___spec__1;
 lean_object* l_Lean_Meta_withLetDecl(lean_object*);
 lean_object* l_Lean_Meta_MetaExtState_inhabited___closed__2;
 size_t l_Lean_Meta_TransparencyMode_hash(uint8_t);
@ -37,6 +38,7 @@ lean_object* l_Lean_Meta_isClassExpensive___main(lean_object*, lean_object*, lea
 lean_object* l_Lean_Meta_throwBug(lean_object*);
 lean_object* l_Lean_MetavarContext_instantiateMVars(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_dbgTrace___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_io_prim_put_str(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_InfoCacheKey_Inhabited;
 lean_object* l_Lean_Meta_getEnv(lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -44,6 +46,7 @@ lean_object* l_Lean_Meta_isReadOnlyExprMVar___boxed(lean_object*, lean_object*,
 lean_object* l_Lean_MetavarContext_addLevelMVarDecl(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_8__forallMetaTelescopeReducingAux___main(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_6__forallTelescopeReducingAux(lean_object*);
+lean_object* l_Lean_Format_pretty(lean_object*, lean_object*);
 extern lean_object* l_EIO_Monad___closed__1;
 lean_object* l_Lean_Meta_savingCache(lean_object*);
 lean_object* l_Lean_Meta_mkFreshExprMVarAt___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -73,15 +76,20 @@ lean_object* l___private_Init_Lean_Meta_Basic_9__lambdaMetaTelescopeAux(lean_obj
 lean_object* l_Lean_Meta_lambdaMetaTelescope___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withLetDecl___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_instantiateLevelMVars(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_MetaHasEval(lean_object*);
 lean_object* l_Lean_Meta_forallBoundedTelescope(lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
+lean_object* l_IO_println___at_Lean_Meta_MetaHasEval___spec__2(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getEnv___boxed(lean_object*);
 lean_object* l_Lean_Meta_hasAssignableMVar___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_MetaHasEval___rarg___closed__2;
 lean_object* l_Lean_Meta_isReducible___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_MessageData_formatAux___main(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_MetaExtState_inhabited___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_instantiateLevelMVars___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_forallTelescope___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forMAux___main___at_Lean_Meta_MetaHasEval___spec__4(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isClassExpensive___main___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
 lean_object* l_Lean_Meta_MetaExtState_inhabited___lambda__2(lean_object*, lean_object*, lean_object*);
@ -98,6 +106,7 @@ lean_object* l_Lean_Meta_mkInferTypeRef___lambda__1(lean_object*, lean_object*,
 lean_object* l_Lean_Meta_isReadOnlyLevelMVar___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_7__lambdaTelescopeAux(lean_object*);
 uint8_t l_Lean_isReducible(lean_object*, lean_object*);
+lean_object* l_Lean_Meta_MetaHasEval___rarg___closed__4;
 lean_object* l_Lean_Meta_InfoCacheKey_Hashable___boxed(lean_object*);
 lean_object* l_Lean_Meta_getConstNoEx(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withMVarContext(lean_object*);
@ -165,6 +174,7 @@ lean_object* l_Lean_Meta_isClassQuickConst___boxed(lean_object*, lean_object*, l
 lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getConstNoEx___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewMCtxDepth___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_MetaHasEval___rarg___closed__3;
 lean_object* l_Lean_Meta_mkMetaExtension___closed__2;
 lean_object* l_Lean_Meta_mkMetaExtension___closed__1;
 lean_object* l_Lean_Meta_mkInferTypeRef___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
@ -175,6 +185,7 @@ lean_object* l_Lean_Meta_dbgTrace___rarg___lambda__1___boxed(lean_object*, lean_
 lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAuxAux___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkSynthPendingRef___lambda__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_MetaHasEval___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescopeReducing___spec__4(lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_3__getTraceState___rarg(lean_object*);
 lean_object* l_Lean_Meta_ParamInfo_inhabited___closed__1;
@ -196,9 +207,9 @@ lean_object* l_Lean_Meta_isReadOnlyExprMVar(lean_object*, lean_object*, lean_obj
 lean_object* l_Lean_Meta_metaExt___closed__1;
 lean_object* l_ReaderT_pure___at_Lean_Meta_MetaExtState_inhabited___spec__1(lean_object*);
 lean_object* l_Lean_Meta_InfoCacheKey_HasBeq___boxed(lean_object*, lean_object*);
+extern lean_object* l_IO_println___rarg___closed__1;
 lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAuxAux___main___at_Lean_Meta_forallBoundedTelescope___spec__2___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_PersistentArray_empty___closed__3;
-lean_object* l_IO_runMeta___rarg___closed__3;
 lean_object* l_Lean_Meta_lambdaMetaTelescope(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkSynthPendingRef___closed__1;
 lean_object* lean_metavar_ctx_assign_expr(lean_object*, lean_object*, lean_object*);
@ -207,6 +218,7 @@ lean_object* l___private_Init_Lean_Meta_Basic_6__forallTelescopeReducingAux___at
 lean_object* l_Lean_Meta_TransparencyMode_HasBeq___closed__1;
 lean_object* l_Lean_Meta_withNewLocalInstances(lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main(lean_object*);
+extern lean_object* l_Lean_Options_empty;
 lean_object* l_Lean_Meta_approxDefEq___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_MetaExtState_inhabited___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescopeReducing___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -241,7 +253,6 @@ uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
 lean_object* l_Lean_Meta_liftStateMCtx___rarg(lean_object*, lean_object*, lean_object*);
 size_t lean_usize_of_nat(lean_object*);
 lean_object* l_Lean_Meta_mkMetaExtension___lambda__1(lean_object*, lean_object*);
-lean_object* l_IO_runMeta___rarg___closed__4;
 lean_object* l_Lean_Meta_usingTransparency(lean_object*);
 lean_object* l_Lean_Meta_withLocalDecl___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_usingAtLeastTransparency___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
@ -263,8 +274,7 @@ lean_object* l_Lean_LocalDecl_type(lean_object*);
 lean_object* lean_local_ctx_mk_local_decl(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
 lean_object* l_Lean_Meta_mkIsExprDefEqAuxRef___lambda__1___closed__1;
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_PersistentHashMap_empty___at_IO_runMeta___spec__1;
-lean_object* l_IO_runMeta___rarg___closed__1;
+lean_object* l_Array_forMAux___main___at_Lean_Meta_MetaHasEval___spec__4___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAuxAux___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkIsExprDefEqAuxRef___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -272,12 +282,14 @@ lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTeles
 lean_object* l_Lean_Meta_withLocalDecl___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallBoundedTelescope___spec__4___rarg___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkIsExprDefEqAuxRef___closed__1;
+lean_object* l_IO_print___at_Lean_Meta_MetaHasEval___spec__3(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_hasAssignableMVar(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAuxAux(lean_object*);
 lean_object* l_Lean_Meta_mkIsExprDefEqAuxRef___lambda__1___closed__2;
 lean_object* l_Lean_Meta_withNewLocalInstances___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAuxAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_ParamInfo_inhabited;
+lean_object* l_Lean_Meta_MetaHasEval___rarg___closed__1;
 lean_object* l_Lean_Meta_metaExt;
 lean_object* l_Lean_Meta_getLocalDecl(lean_object*, lean_object*, lean_object*);
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
@ -296,7 +308,6 @@ lean_object* l_Lean_Meta_synthPendingRef;
 lean_object* l_Lean_Meta_getConstAux(lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* lean_metavar_ctx_assign_level(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_throwEx___rarg___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* l_IO_runMeta___rarg___closed__2;
 lean_object* l_Lean_Meta_withMVarContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_1__whenDebugging___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_incDepth(lean_object*);
@ -324,7 +335,6 @@ lean_object* l_Lean_Meta_dbgTrace(lean_object*);
 lean_object* l___private_Init_Lean_Util_Trace_4__checkTraceOption___at_Lean_Meta_trace___spec__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkFreshId(lean_object*);
 lean_object* l_Lean_Meta_usingTransparency___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
-lean_object* l_PersistentHashMap_empty___at_IO_runMeta___spec__1___closed__1;
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAuxAux___main___at_Lean_Meta_forallBoundedTelescope___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_TransparencyMode_beq___boxed(lean_object*, lean_object*);
@ -368,6 +378,7 @@ lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAuxAux__
 lean_object* l_Lean_Meta_mkWHNFRef___closed__1;
 lean_object* l_Lean_Meta_mkFreshLevelMVar___rarg(lean_object*);
 extern lean_object* l_Lean_MetavarContext_Inhabited___closed__1;
+lean_object* l_PersistentHashMap_empty___at_Lean_Meta_MetaHasEval___spec__1___closed__1;
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__3(lean_object*);
 lean_object* l_Lean_Meta_mkMetaExtension___closed__3;
 lean_object* l_Lean_Meta_isClassQuick___main___closed__1;
@ -45778,7 +45789,7 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Meta_withMCtx___rarg), 4, 0);
 return x_2;
 }
 }
-lean_object* _init_l_PersistentHashMap_empty___at_IO_runMeta___spec__1___closed__1() {
+lean_object* _init_l_PersistentHashMap_empty___at_Lean_Meta_MetaHasEval___spec__1___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@ -45790,15 +45801,128 @@ lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_PersistentHashMap_empty___at_IO_runMeta___spec__1() {
+lean_object* _init_l_PersistentHashMap_empty___at_Lean_Meta_MetaHasEval___spec__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_PersistentHashMap_empty___at_IO_runMeta___spec__1___closed__1;
+x_1 = l_PersistentHashMap_empty___at_Lean_Meta_MetaHasEval___spec__1___closed__1;
 return x_1;
 }
 }
-lean_object* _init_l_IO_runMeta___rarg___closed__1() {
+lean_object* l_IO_print___at_Lean_Meta_MetaHasEval___spec__3(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_3 = l_Lean_Options_empty;
+x_4 = l_Lean_Format_pretty(x_1, x_3);
+x_5 = lean_io_prim_put_str(x_4, x_2);
+lean_dec(x_4);
+return x_5;
+}
+}
+lean_object* l_IO_println___at_Lean_Meta_MetaHasEval___spec__2(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_IO_print___at_Lean_Meta_MetaHasEval___spec__3(x_1, x_2);
+if (lean_obj_tag(x_3) == 0)
+{
+lean_object* x_4; lean_object* x_5; lean_object* x_6; 
+x_4 = lean_ctor_get(x_3, 1);
+lean_inc(x_4);
+lean_dec(x_3);
+x_5 = l_IO_println___rarg___closed__1;
+x_6 = lean_io_prim_put_str(x_5, x_4);
+return x_6;
+}
+else
+{
+uint8_t x_7; 
+x_7 = !lean_is_exclusive(x_3);
+if (x_7 == 0)
+{
+return x_3;
+}
+else
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; 
+x_8 = lean_ctor_get(x_3, 0);
+x_9 = lean_ctor_get(x_3, 1);
+lean_inc(x_9);
+lean_inc(x_8);
+lean_dec(x_3);
+x_10 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_10, 0, x_8);
+lean_ctor_set(x_10, 1, x_9);
+return x_10;
+}
+}
+}
+}
+lean_object* l_Array_forMAux___main___at_Lean_Meta_MetaHasEval___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; uint8_t x_5; 
+x_4 = lean_array_get_size(x_1);
+x_5 = lean_nat_dec_lt(x_2, x_4);
+lean_dec(x_4);
+if (x_5 == 0)
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_2);
+x_6 = lean_box(0);
+x_7 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_7, 0, x_6);
+lean_ctor_set(x_7, 1, x_3);
+return x_7;
+}
+else
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+x_8 = lean_array_fget(x_1, x_2);
+x_9 = lean_unsigned_to_nat(1u);
+x_10 = lean_nat_add(x_2, x_9);
+lean_dec(x_2);
+x_11 = lean_box(0);
+x_12 = l_Lean_MessageData_formatAux___main(x_11, x_8);
+x_13 = l_IO_println___at_Lean_Meta_MetaHasEval___spec__2(x_12, x_3);
+if (lean_obj_tag(x_13) == 0)
+{
+lean_object* x_14; 
+x_14 = lean_ctor_get(x_13, 1);
+lean_inc(x_14);
+lean_dec(x_13);
+x_2 = x_10;
+x_3 = x_14;
+goto _start;
+}
+else
+{
+uint8_t x_16; 
+lean_dec(x_10);
+x_16 = !lean_is_exclusive(x_13);
+if (x_16 == 0)
+{
+return x_13;
+}
+else
+{
+lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+x_17 = lean_ctor_get(x_13, 0);
+x_18 = lean_ctor_get(x_13, 1);
+lean_inc(x_18);
+lean_inc(x_17);
+lean_dec(x_13);
+x_19 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_19, 0, x_17);
+lean_ctor_set(x_19, 1, x_18);
+return x_19;
+}
+}
+}
+}
+}
+lean_object* _init_l_Lean_Meta_MetaHasEval___rarg___closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -45806,7 +45930,7 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Meta_InfoCacheKey_Hashable___boxed), 1,
 return x_1;
 }
 }
-lean_object* _init_l_IO_runMeta___rarg___closed__2() {
+lean_object* _init_l_Lean_Meta_MetaHasEval___rarg___closed__2() {
 _start:
 {
 lean_object* x_1; 
@ -45814,7 +45938,7 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Meta_InfoCacheKey_HasBeq___boxed), 2, 0)
 return x_1;
 }
 }
-lean_object* _init_l_IO_runMeta___rarg___closed__3() {
+lean_object* _init_l_Lean_Meta_MetaHasEval___rarg___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@ -45826,12 +45950,12 @@ lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_IO_runMeta___rarg___closed__4() {
+lean_object* _init_l_Lean_Meta_MetaHasEval___rarg___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_PersistentHashMap_empty___at_IO_runMeta___spec__1;
-x_2 = l_IO_runMeta___rarg___closed__3;
+x_1 = l_PersistentHashMap_empty___at_Lean_Meta_MetaHasEval___spec__1;
+x_2 = l_Lean_Meta_MetaHasEval___rarg___closed__3;
 x_3 = l_Lean_Meta_resettingSynthInstanceCache___rarg___closed__1;
 x_4 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
@ -45840,6 +45964,184 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
+lean_object* l_Lean_Meta_MetaHasEval___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+uint8_t x_6; uint8_t x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_6 = 0;
+x_7 = 1;
+lean_inc(x_3);
+x_8 = lean_alloc_ctor(0, 1, 6);
+lean_ctor_set(x_8, 0, x_3);
+lean_ctor_set_uint8(x_8, sizeof(void*)*1, x_6);
+lean_ctor_set_uint8(x_8, sizeof(void*)*1 + 1, x_6);
+lean_ctor_set_uint8(x_8, sizeof(void*)*1 + 2, x_6);
+lean_ctor_set_uint8(x_8, sizeof(void*)*1 + 3, x_6);
+lean_ctor_set_uint8(x_8, sizeof(void*)*1 + 4, x_6);
+lean_ctor_set_uint8(x_8, sizeof(void*)*1 + 5, x_7);
+x_9 = l_Lean_LocalContext_Inhabited___closed__2;
+x_10 = l_Array_empty___closed__1;
+x_11 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_11, 0, x_8);
+lean_ctor_set(x_11, 1, x_9);
+lean_ctor_set(x_11, 2, x_10);
+x_12 = l_Lean_MetavarContext_Inhabited___closed__1;
+x_13 = l_Lean_Meta_MetaHasEval___rarg___closed__4;
+x_14 = l_Lean_NameGenerator_Inhabited___closed__3;
+x_15 = l_Lean_TraceState_Inhabited___closed__1;
+x_16 = l_PersistentArray_empty___closed__3;
+x_17 = lean_alloc_ctor(0, 6, 0);
+lean_ctor_set(x_17, 0, x_2);
+lean_ctor_set(x_17, 1, x_12);
+lean_ctor_set(x_17, 2, x_13);
+lean_ctor_set(x_17, 3, x_14);
+lean_ctor_set(x_17, 4, x_15);
+lean_ctor_set(x_17, 5, x_16);
+x_18 = lean_apply_2(x_4, x_11, x_17);
+if (lean_obj_tag(x_18) == 0)
+{
+lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+x_19 = lean_ctor_get(x_18, 0);
+lean_inc(x_19);
+x_20 = lean_ctor_get(x_18, 1);
+lean_inc(x_20);
+lean_dec(x_18);
+x_21 = lean_ctor_get(x_20, 4);
+lean_inc(x_21);
+x_22 = lean_ctor_get(x_21, 0);
+lean_inc(x_22);
+lean_dec(x_21);
+x_23 = lean_unsigned_to_nat(0u);
+x_24 = l_Array_forMAux___main___at_Lean_Meta_MetaHasEval___spec__4(x_22, x_23, x_5);
+lean_dec(x_22);
+if (lean_obj_tag(x_24) == 0)
+{
+lean_object* x_25; lean_object* x_26; lean_object* x_27; 
+x_25 = lean_ctor_get(x_24, 1);
+lean_inc(x_25);
+lean_dec(x_24);
+x_26 = lean_ctor_get(x_20, 0);
+lean_inc(x_26);
+lean_dec(x_20);
+x_27 = lean_apply_4(x_1, x_26, x_3, x_19, x_25);
+return x_27;
+}
+else
+{
+uint8_t x_28; 
+lean_dec(x_20);
+lean_dec(x_19);
+lean_dec(x_3);
+lean_dec(x_1);
+x_28 = !lean_is_exclusive(x_24);
+if (x_28 == 0)
+{
+return x_24;
+}
+else
+{
+lean_object* x_29; lean_object* x_30; lean_object* x_31; 
+x_29 = lean_ctor_get(x_24, 0);
+x_30 = lean_ctor_get(x_24, 1);
+lean_inc(x_30);
+lean_inc(x_29);
+lean_dec(x_24);
+x_31 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_31, 0, x_29);
+lean_ctor_set(x_31, 1, x_30);
+return x_31;
+}
+}
+}
+else
+{
+lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; 
+lean_dec(x_3);
+lean_dec(x_1);
+x_32 = lean_ctor_get(x_18, 0);
+lean_inc(x_32);
+x_33 = lean_ctor_get(x_18, 1);
+lean_inc(x_33);
+lean_dec(x_18);
+x_34 = lean_ctor_get(x_33, 4);
+lean_inc(x_34);
+lean_dec(x_33);
+x_35 = lean_ctor_get(x_34, 0);
+lean_inc(x_35);
+lean_dec(x_34);
+x_36 = lean_unsigned_to_nat(0u);
+x_37 = l_Array_forMAux___main___at_Lean_Meta_MetaHasEval___spec__4(x_35, x_36, x_5);
+lean_dec(x_35);
+if (lean_obj_tag(x_37) == 0)
+{
+uint8_t x_38; 
+x_38 = !lean_is_exclusive(x_37);
+if (x_38 == 0)
+{
+lean_object* x_39; lean_object* x_40; 
+x_39 = lean_ctor_get(x_37, 0);
+lean_dec(x_39);
+x_40 = l_Lean_Meta_Exception_toStr(x_32);
+lean_ctor_set_tag(x_37, 1);
+lean_ctor_set(x_37, 0, x_40);
+return x_37;
+}
+else
+{
+lean_object* x_41; lean_object* x_42; lean_object* x_43; 
+x_41 = lean_ctor_get(x_37, 1);
+lean_inc(x_41);
+lean_dec(x_37);
+x_42 = l_Lean_Meta_Exception_toStr(x_32);
+x_43 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_43, 0, x_42);
+lean_ctor_set(x_43, 1, x_41);
+return x_43;
+}
+}
+else
+{
+uint8_t x_44; 
+lean_dec(x_32);
+x_44 = !lean_is_exclusive(x_37);
+if (x_44 == 0)
+{
+return x_37;
+}
+else
+{
+lean_object* x_45; lean_object* x_46; lean_object* x_47; 
+x_45 = lean_ctor_get(x_37, 0);
+x_46 = lean_ctor_get(x_37, 1);
+lean_inc(x_46);
+lean_inc(x_45);
+lean_dec(x_37);
+x_47 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_47, 0, x_45);
+lean_ctor_set(x_47, 1, x_46);
+return x_47;
+}
+}
+}
+}
+}
+lean_object* l_Lean_Meta_MetaHasEval(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Meta_MetaHasEval___rarg), 5, 0);
+return x_2;
+}
+}
+lean_object* l_Array_forMAux___main___at_Lean_Meta_MetaHasEval___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Array_forMAux___main___at_Lean_Meta_MetaHasEval___spec__4(x_1, x_2, x_3);
+lean_dec(x_1);
+return x_4;
+}
+}
 lean_object* l_IO_runMeta___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
@ -45851,7 +46153,7 @@ lean_ctor_set(x_7, 0, x_3);
 lean_ctor_set(x_7, 1, x_5);
 lean_ctor_set(x_7, 2, x_6);
 x_8 = l_Lean_MetavarContext_Inhabited___closed__1;
-x_9 = l_IO_runMeta___rarg___closed__4;
+x_9 = l_Lean_Meta_MetaHasEval___rarg___closed__4;
 x_10 = l_Lean_NameGenerator_Inhabited___closed__3;
 x_11 = l_Lean_TraceState_Inhabited___closed__1;
 x_12 = l_PersistentArray_empty___closed__3;
@ -45949,6 +46251,7 @@ lean_object* initialize_Init_Lean_ReducibilityAttrs(lean_object*);
 lean_object* initialize_Init_Lean_Util_Trace(lean_object*);
 lean_object* initialize_Init_Lean_Meta_Exception(lean_object*);
 lean_object* initialize_Init_Lean_Meta_DiscrTreeTypes(lean_object*);
+lean_object* initialize_Init_Lean_Eval(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean_Meta_Basic(lean_object* w) {
 lean_object * res;
@ -45981,6 +46284,9 @@ lean_dec_ref(res);
 res = initialize_Init_Lean_Meta_DiscrTreeTypes(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Eval(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 l_Lean_Meta_TransparencyMode_Inhabited = _init_l_Lean_Meta_TransparencyMode_Inhabited();
 l_Lean_Meta_TransparencyMode_HasBeq___closed__1 = _init_l_Lean_Meta_TransparencyMode_HasBeq___closed__1();
 lean_mark_persistent(l_Lean_Meta_TransparencyMode_HasBeq___closed__1);
@ -46083,18 +46389,18 @@ l_Lean_Meta_isClassQuick___main___closed__1 = _init_l_Lean_Meta_isClassQuick___m
 lean_mark_persistent(l_Lean_Meta_isClassQuick___main___closed__1);
 l_Lean_Meta_resettingSynthInstanceCache___rarg___closed__1 = _init_l_Lean_Meta_resettingSynthInstanceCache___rarg___closed__1();
 lean_mark_persistent(l_Lean_Meta_resettingSynthInstanceCache___rarg___closed__1);
-l_PersistentHashMap_empty___at_IO_runMeta___spec__1___closed__1 = _init_l_PersistentHashMap_empty___at_IO_runMeta___spec__1___closed__1();
-lean_mark_persistent(l_PersistentHashMap_empty___at_IO_runMeta___spec__1___closed__1);
-l_PersistentHashMap_empty___at_IO_runMeta___spec__1 = _init_l_PersistentHashMap_empty___at_IO_runMeta___spec__1();
-lean_mark_persistent(l_PersistentHashMap_empty___at_IO_runMeta___spec__1);
-l_IO_runMeta___rarg___closed__1 = _init_l_IO_runMeta___rarg___closed__1();
-lean_mark_persistent(l_IO_runMeta___rarg___closed__1);
-l_IO_runMeta___rarg___closed__2 = _init_l_IO_runMeta___rarg___closed__2();
-lean_mark_persistent(l_IO_runMeta___rarg___closed__2);
-l_IO_runMeta___rarg___closed__3 = _init_l_IO_runMeta___rarg___closed__3();
-lean_mark_persistent(l_IO_runMeta___rarg___closed__3);
-l_IO_runMeta___rarg___closed__4 = _init_l_IO_runMeta___rarg___closed__4();
-lean_mark_persistent(l_IO_runMeta___rarg___closed__4);
+l_PersistentHashMap_empty___at_Lean_Meta_MetaHasEval___spec__1___closed__1 = _init_l_PersistentHashMap_empty___at_Lean_Meta_MetaHasEval___spec__1___closed__1();
+lean_mark_persistent(l_PersistentHashMap_empty___at_Lean_Meta_MetaHasEval___spec__1___closed__1);
+l_PersistentHashMap_empty___at_Lean_Meta_MetaHasEval___spec__1 = _init_l_PersistentHashMap_empty___at_Lean_Meta_MetaHasEval___spec__1();
+lean_mark_persistent(l_PersistentHashMap_empty___at_Lean_Meta_MetaHasEval___spec__1);
+l_Lean_Meta_MetaHasEval___rarg___closed__1 = _init_l_Lean_Meta_MetaHasEval___rarg___closed__1();
+lean_mark_persistent(l_Lean_Meta_MetaHasEval___rarg___closed__1);
+l_Lean_Meta_MetaHasEval___rarg___closed__2 = _init_l_Lean_Meta_MetaHasEval___rarg___closed__2();
+lean_mark_persistent(l_Lean_Meta_MetaHasEval___rarg___closed__2);
+l_Lean_Meta_MetaHasEval___rarg___closed__3 = _init_l_Lean_Meta_MetaHasEval___rarg___closed__3();
+lean_mark_persistent(l_Lean_Meta_MetaHasEval___rarg___closed__3);
+l_Lean_Meta_MetaHasEval___rarg___closed__4 = _init_l_Lean_Meta_MetaHasEval___rarg___closed__4();
+lean_mark_persistent(l_Lean_Meta_MetaHasEval___rarg___closed__4);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus
--- a/stage0/stdlib/Init/Lean/Meta/Instances.c
+++ b/stage0/stdlib/Init/Lean/Meta/Instances.c
@ -55,6 +55,7 @@ size_t l_USize_shiftRight(size_t, size_t);
 lean_object* l_Array_iterateMAux___main___at_Lean_Meta_mkInstanceExtension___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_findAux___main___at_Lean_Meta_addInstanceEntry___spec__3___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_instanceExtension___elambda__3___boxed(lean_object*, lean_object*);
+extern lean_object* l_Lean_Meta_MetaHasEval___rarg___closed__4;
 uint8_t l_Lean_Meta_DiscrTree_Key_beq(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_IO_ofExcept___at_Lean_registerClassAttr___spec__1(lean_object*, lean_object*);
@ -105,7 +106,6 @@ size_t l_USize_mul(size_t, size_t);
 lean_object* l_Lean_Meta_instanceExtension___closed__1;
 lean_object* l_Lean_Meta_registerInstanceAttr___closed__6;
 lean_object* l_Lean_Meta_instanceExtension___closed__2;
-extern lean_object* l_IO_runMeta___rarg___closed__4;
 lean_object* l_Lean_Meta_registerInstanceAttr___lambda__1___closed__2;
 lean_object* lean_add_instance(lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
@ -3236,7 +3236,7 @@ lean_dec(x_7);
 x_9 = l_List_map___main___at_Lean_Meta_addGlobalInstance___spec__1(x_8);
 x_10 = l_Lean_mkConst(x_2, x_9);
 x_11 = l_Lean_MetavarContext_Inhabited___closed__1;
-x_12 = l_IO_runMeta___rarg___closed__4;
+x_12 = l_Lean_Meta_MetaHasEval___rarg___closed__4;
 x_13 = l_Lean_NameGenerator_Inhabited___closed__3;
 x_14 = l_Lean_TraceState_Inhabited___closed__1;
 x_15 = l_PersistentArray_empty___closed__3;
--- a/stage0/stdlib/Init/Lean/MonadCache.c
+++ b/stage0/stdlib/Init/Lean/MonadCache.c
--- a/stage0/stdlib/Init/Lean/Path.c
+++ b/stage0/stdlib/Init/Lean/Path.c
--- a/stage0/stdlib/Init/Lean/Trace.c
+++ b/stage0/stdlib/Init/Lean/Trace.c
--- a/stage0/stdlib/Init/Lean/Util.c
+++ b/stage0/stdlib/Init/Lean/Util.c
@ -1,77 +0,0 @@
-// Lean compiler output
-// Module: Init.Lean.Util
-// Imports: Init.System.IO Init.Lean.Data.Position
-#include "runtime/lean.h"
-#if defined(__clang__)
-#pragma clang diagnostic ignored "-Wunused-parameter"
-#pragma clang diagnostic ignored "-Wunused-label"
-#elif defined(__GNUC__) && !defined(__CLANG__)
-#pragma GCC diagnostic ignored "-Wunused-parameter"
-#pragma GCC diagnostic ignored "-Wunused-label"
-#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
-#endif
-#ifdef __cplusplus
-extern "C" {
-#endif
-lean_object* lean_lean_profileit(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_IO_lazyPure___rarg(lean_object*, lean_object*);
-lean_object* l_Lean_profileitPure___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_profileit___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_profileitPure(lean_object*);
-lean_object* l_Lean_profileitPure___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_profileit___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
-_start:
-{
-lean_object* x_6; 
-x_6 = lean_lean_profileit(x_2, x_3, x_4, x_5);
-lean_dec(x_3);
-lean_dec(x_2);
-return x_6;
-}
-}
-lean_object* l_Lean_profileitPure___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-lean_object* x_5; lean_object* x_6; 
-x_5 = lean_alloc_closure((void*)(l_IO_lazyPure___rarg), 2, 1);
-lean_closure_set(x_5, 0, x_3);
-x_6 = lean_lean_profileit(x_1, x_2, x_5, x_4);
-return x_6;
-}
-}
-lean_object* l_Lean_profileitPure(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Lean_profileitPure___rarg___boxed), 4, 0);
-return x_2;
-}
-}
-lean_object* l_Lean_profileitPure___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-lean_object* x_5; 
-x_5 = l_Lean_profileitPure___rarg(x_1, x_2, x_3, x_4);
-lean_dec(x_2);
-lean_dec(x_1);
-return x_5;
-}
-}
-lean_object* initialize_Init_System_IO(lean_object*);
-lean_object* initialize_Init_Lean_Data_Position(lean_object*);
-static bool _G_initialized = false;
-lean_object* initialize_Init_Lean_Util(lean_object* w) {
-lean_object * res;
-if (_G_initialized) return lean_mk_io_result(lean_box(0));
-_G_initialized = true;
-res = initialize_Init_System_IO(lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Init_Lean_Data_Position(lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-return lean_mk_io_result(lean_box(0));
-}
-#ifdef __cplusplus
-}
-#endif
--- a/stage0/stdlib/Init/Lean/WHNF.c
+++ b/stage0/stdlib/Init/Lean/WHNF.c
--- a/stage0/stdlib/Init/System/IO.c
+++ b/stage0/stdlib/Init/System/IO.c
@ -13,8 +13,7 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
-lean_object* l_IO_HasEval___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Init_System_IO_1__putStr___at_HasRepr_HasEval___spec__3___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_IOUnit_HasEval(lean_object*, lean_object*);
 lean_object* l___private_Init_System_IO_1__putStr(lean_object*, lean_object*);
 lean_object* l_allocprof___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_mkRef___boxed(lean_object*, lean_object*);
@ -56,13 +55,12 @@ lean_object* l_IO_Ref_swap___rarg(lean_object*, lean_object*, lean_object*, lean
 lean_object* l_IO_Error_HasToString;
 lean_object* l_EIO_Inhabited(lean_object*, lean_object*);
 lean_object* l_IO_Fs_handle_close(lean_object*, lean_object*);
+lean_object* l___private_Init_System_IO_1__putStr___at_Lean_HasRepr_HasEval___spec__3___boxed(lean_object*, lean_object*);
 lean_object* l_IO_Fs_handle_getLine___at_IO_Fs_handle_readToEnd___spec__2___boxed(lean_object*, lean_object*);
 lean_object* lean_io_getenv(lean_object*, lean_object*);
 lean_object* l_IO_Fs_readFile(lean_object*);
-lean_object* l_IO_println___at_HasRepr_HasEval___spec__1(lean_object*, lean_object*);
 lean_object* l_IO_Ref_get___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Init_System_IO_1__putStr___at_HasRepr_HasEval___spec__3(lean_object*, lean_object*);
-lean_object* l_IOUnit_HasEval(lean_object*, lean_object*);
+lean_object* l_Lean_HasRepr_HasEval(lean_object*);
 lean_object* l_IO_readTextFile___rarg(lean_object*, lean_object*);
 lean_object* l_EIO_Inhabited___rarg(lean_object*);
 lean_object* l_IO_Fs_handle_isEof(lean_object*, lean_object*);
@ -84,8 +82,8 @@ lean_object* l_IO_Prim_liftIO___rarg(lean_object*, lean_object*);
 lean_object* l_EIO_MonadExcept(lean_object*);
 lean_object* l_finally___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_Ref_reset___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* l_IO_HasEval(lean_object*);
 lean_object* l_IO_Prim_handle_isEof___boxed(lean_object*, lean_object*);
+lean_object* l_IO_println___at_Lean_HasRepr_HasEval___spec__1(lean_object*, lean_object*);
 lean_object* l_IO_realPath___boxed(lean_object*, lean_object*);
 lean_object* lean_io_realpath(lean_object*, lean_object*);
 lean_object* l_System_FilePath_dirName(lean_object*);
@ -102,13 +100,11 @@ lean_object* l_IO_Prim_liftIO___boxed(lean_object*, lean_object*);
 lean_object* l_IO_Prim_getLine___boxed(lean_object*);
 lean_object* l_IO_println___rarg___closed__1;
 lean_object* l_IO_initializing___boxed(lean_object*);
+lean_object* l___private_Init_System_IO_1__putStr___at_Lean_HasRepr_HasEval___spec__3(lean_object*, lean_object*);
 lean_object* l_IO_Prim_iterate(lean_object*, lean_object*);
 lean_object* l_IO_Prim_iterate___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* l_IO_print___at_HasRepr_HasEval___spec__2(lean_object*, lean_object*);
-lean_object* l_HasRepr_HasEval(lean_object*);
 lean_object* lean_io_prim_handle_get_line(lean_object*, lean_object*);
 lean_object* l_IO_println___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_IO_print___at_HasRepr_HasEval___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_IO_isDir___boxed(lean_object*, lean_object*);
 lean_object* l_IO_Fs_handle_close___boxed(lean_object*, lean_object*);
 lean_object* l_IO_fileExists___rarg(lean_object*, lean_object*);
@ -130,17 +126,19 @@ lean_object* l_IO_Fs_handle_mk___boxed(lean_object*, lean_object*);
 lean_object* l_EIO_HasOrelse___closed__1;
 lean_object* l_IO_ofExcept(lean_object*, lean_object*);
 lean_object* lean_io_file_exists(lean_object*, lean_object*);
+lean_object* l_Lean_IO_HasEval(lean_object*);
 lean_object* l_EStateM_nonBacktrackable(lean_object*);
-lean_object* l_IO_println___at_HasRepr_HasEval___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_IO_Fs_handle_isEof___boxed(lean_object*, lean_object*);
 lean_object* l_IO_Fs_handle_getLine(lean_object*, lean_object*);
 lean_object* l_IO_Prim_isDir___boxed(lean_object*, lean_object*);
 lean_object* l_IO_isDir___rarg(lean_object*, lean_object*);
 lean_object* l_IO_getEnv(lean_object*, lean_object*);
 lean_object* l_IO_Ref_modify___boxed(lean_object*);
+lean_object* l_IO_print___at_Lean_HasRepr_HasEval___spec__2(lean_object*, lean_object*);
 lean_object* l_IO_lazyPure(lean_object*);
 lean_object* l_EStateM_Monad(lean_object*, lean_object*);
 lean_object* l_MonadExcept_orelse___at_EIO_HasOrelse___spec__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_IO_println___at_Lean_HasRepr_HasEval___spec__1___boxed(lean_object*, lean_object*);
 lean_object* lean_io_prim_handle_is_eof(lean_object*, lean_object*);
 lean_object* lean_io_prim_handle_mk(lean_object*, uint8_t, uint8_t, lean_object*);
 lean_object* l_IO_Fs_handle_mk(lean_object*, lean_object*);
@ -153,6 +151,7 @@ lean_object* lean_io_ref_swap(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_getEnv___boxed(lean_object*, lean_object*);
 lean_object* l_IO_Fs_readFile___rarg(lean_object*, lean_object*, lean_object*, uint8_t);
 lean_object* l_IO_print___boxed(lean_object*, lean_object*);
+lean_object* l_IO_print___at_Lean_HasRepr_HasEval___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_IO_Ref_swap(lean_object*, lean_object*);
 lean_object* l_IO_Prim_Ref_swap___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_io_ref_set(lean_object*, lean_object*, lean_object*);
@ -160,6 +159,7 @@ lean_object* l_IO_appDir___rarg___lambda__1(lean_object*, lean_object*);
 lean_object* l_IO_Ref_reset___boxed(lean_object*, lean_object*);
 lean_object* l_IO_Fs_handle_getLine___at_IO_Fs_handle_readToEnd___spec__2(lean_object*, lean_object*);
 lean_object* l_EStateM_MonadExcept___rarg(lean_object*);
+lean_object* l_Lean_HasRepr_HasEval___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EIO_MonadExcept___closed__2;
 lean_object* lean_io_prim_read_text_file(lean_object*, lean_object*);
 lean_object* l_IO_Fs_handle_flush___boxed(lean_object*, lean_object*);
@ -172,6 +172,7 @@ lean_object* l_IO_mkRef(lean_object*, lean_object*);
 lean_object* l_MonadExcept_orelse___at_EIO_HasOrelse___spec__1(lean_object*, lean_object*);
 lean_object* l_EIO_Monad(lean_object*);
 lean_object* l___private_Init_System_IO_1__putStr___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_IO_HasEval___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_timeit___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_io_app_dir(lean_object*);
 lean_object* l_IO_Fs_readFile___boxed(lean_object*);
@ -192,7 +193,6 @@ lean_object* l_IO_Fs_handle_mk___rarg___boxed(lean_object*, lean_object*, lean_o
 lean_object* l_IO_Fs_handle_flush___rarg(lean_object*, lean_object*);
 lean_object* l_IO_appDir___rarg(lean_object*, lean_object*);
 lean_object* l_IO_Prim_iterate___main___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* l_HasRepr_HasEval___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_Ref_reset(lean_object*, lean_object*);
 lean_object* l_IO_Fs_handle_isEof___rarg(lean_object*, lean_object*);
 lean_object* _init_l_EIO_Monad___closed__1() {
@ -1741,7 +1741,7 @@ lean_dec(x_1);
 return x_2;
 }
 }
-lean_object* l___private_Init_System_IO_1__putStr___at_HasRepr_HasEval___spec__3(lean_object* x_1, lean_object* x_2) {
+lean_object* l___private_Init_System_IO_1__putStr___at_Lean_HasRepr_HasEval___spec__3(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
@ -1749,7 +1749,7 @@ x_3 = lean_io_prim_put_str(x_1, x_2);
 return x_3;
 }
 }
-lean_object* l_IO_print___at_HasRepr_HasEval___spec__2(lean_object* x_1, lean_object* x_2) {
+lean_object* l_IO_print___at_Lean_HasRepr_HasEval___spec__2(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
@ -1757,7 +1757,7 @@ x_3 = lean_io_prim_put_str(x_1, x_2);
 return x_3;
 }
 }
-lean_object* l_IO_println___at_HasRepr_HasEval___spec__1(lean_object* x_1, lean_object* x_2) {
+lean_object* l_IO_println___at_Lean_HasRepr_HasEval___spec__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
@ -1796,52 +1796,52 @@ return x_10;
 }
 }
 }
-lean_object* l_HasRepr_HasEval___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_HasRepr_HasEval___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; lean_object* x_5; 
 x_4 = lean_apply_1(x_1, x_2);
-x_5 = l_IO_println___at_HasRepr_HasEval___spec__1(x_4, x_3);
+x_5 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_4, x_3);
 lean_dec(x_4);
 return x_5;
 }
 }
-lean_object* l_HasRepr_HasEval(lean_object* x_1) {
+lean_object* l_Lean_HasRepr_HasEval(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_HasRepr_HasEval___rarg), 3, 0);
+x_2 = lean_alloc_closure((void*)(l_Lean_HasRepr_HasEval___rarg), 3, 0);
 return x_2;
 }
 }
-lean_object* l___private_Init_System_IO_1__putStr___at_HasRepr_HasEval___spec__3___boxed(lean_object* x_1, lean_object* x_2) {
+lean_object* l___private_Init_System_IO_1__putStr___at_Lean_HasRepr_HasEval___spec__3___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = l___private_Init_System_IO_1__putStr___at_HasRepr_HasEval___spec__3(x_1, x_2);
+x_3 = l___private_Init_System_IO_1__putStr___at_Lean_HasRepr_HasEval___spec__3(x_1, x_2);
 lean_dec(x_1);
 return x_3;
 }
 }
-lean_object* l_IO_print___at_HasRepr_HasEval___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
+lean_object* l_IO_print___at_Lean_HasRepr_HasEval___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = l_IO_print___at_HasRepr_HasEval___spec__2(x_1, x_2);
+x_3 = l_IO_print___at_Lean_HasRepr_HasEval___spec__2(x_1, x_2);
 lean_dec(x_1);
 return x_3;
 }
 }
-lean_object* l_IO_println___at_HasRepr_HasEval___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
+lean_object* l_IO_println___at_Lean_HasRepr_HasEval___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = l_IO_println___at_HasRepr_HasEval___spec__1(x_1, x_2);
+x_3 = l_IO_println___at_Lean_HasRepr_HasEval___spec__1(x_1, x_2);
 lean_dec(x_1);
 return x_3;
 }
 }
-lean_object* l_IO_HasEval___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_IO_HasEval___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; 
@ -1882,15 +1882,15 @@ return x_11;
 }
 }
 }
-lean_object* l_IO_HasEval(lean_object* x_1) {
+lean_object* l_Lean_IO_HasEval(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_IO_HasEval___rarg), 3, 0);
+x_2 = lean_alloc_closure((void*)(l_Lean_IO_HasEval___rarg), 3, 0);
 return x_2;
 }
 }
-lean_object* l_IOUnit_HasEval(lean_object* x_1, lean_object* x_2) {
+lean_object* l_Lean_IOUnit_HasEval(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3;