From 99e3cdc01ba934be5755cf07cf1c77fda0834942 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 13 May 2019 13:03:14 -0700
Subject: [PATCH] chore(frontends/lean): delete `lean_environment`

---
 src/frontends/lean/CMakeLists.txt           |   3 +-
 src/frontends/lean/init_module.cpp          |   3 -
 src/frontends/lean/lean_elaborator.cpp      |  19 +-
 src/frontends/lean/lean_environment.cpp     |  65 --
 src/frontends/lean/lean_environment.h       |  17 -
 src/kernel/environment.cpp                  |  16 +-
 src/shell/lean.cpp                          |   5 +-
 src/stage0/init/lean/elaborator.cpp         | 639 +++++++++-----------
 src/stage0/init/lean/environment.cpp        |  35 ++
 src/stage0/init/lean/expander.cpp           |  56 +-
 src/stage0/init/lean/parser/command.cpp     | 226 +++----
 src/stage0/init/lean/parser/declaration.cpp | 212 +++----
 src/util/object_ref.h                       |   2 +-
 13 files changed, 604 insertions(+), 694 deletions(-)
 delete mode 100644 src/frontends/lean/lean_environment.cpp
 delete mode 100644 src/frontends/lean/lean_environment.h

diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index 50e2ce010c..ceb371b5cb 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -6,5 +6,4 @@ inductive_cmds.cpp pp.cpp structure_cmd.cpp structure_instance.cpp
 init_module.cpp type_util.cpp decl_attributes.cpp
 prenum.cpp print_cmd.cpp elaborator.cpp
 match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
-brackets.cpp json.cpp typed_expr.cpp choice.cpp lean_elaborator.cpp
-lean_environment.cpp)
+brackets.cpp json.cpp typed_expr.cpp choice.cpp lean_elaborator.cpp)
diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp
index 2d797bab63..09b7813aaa 100644
--- a/src/frontends/lean/init_module.cpp
+++ b/src/frontends/lean/init_module.cpp
@@ -24,7 +24,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/util.h"
 #include "frontends/lean/brackets.h"
 #include "frontends/lean/choice.h"
-#include "frontends/lean/lean_environment.h"
 
 namespace lean {
 void initialize_frontend_lean_module() {
@@ -48,10 +47,8 @@ void initialize_frontend_lean_module() {
     initialize_notation_cmd();
     initialize_frontend_lean_util();
     initialize_brackets();
-    initialize_lean_environment();
 }
 void finalize_frontend_lean_module() {
-    finalize_lean_environment();
     finalize_brackets();
     finalize_frontend_lean_util();
     finalize_notation_cmd();
diff --git a/src/frontends/lean/lean_elaborator.cpp b/src/frontends/lean/lean_elaborator.cpp
index fb933bce81..4daf797a88 100644
--- a/src/frontends/lean/lean_elaborator.cpp
+++ b/src/frontends/lean/lean_elaborator.cpp
@@ -27,7 +27,6 @@ Lean interface to the old elaborator/elaboration parts of the parser
 #include "frontends/lean/util.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/simple_pos_info_provider.h"
-#include "frontends/lean/lean_environment.h"
 
 namespace lean {
 struct resolve_names_fn : public replace_visitor {
@@ -454,7 +453,7 @@ object_ref to_obj(name_generator const & ngen) {
 // TODO(Sebastian): replace `string` with `message` in the new runtime
 extern "C" obj_res lean_elaborator_elaborate_command(b_obj_arg vm_filename, obj_arg vm_cmd, b_obj_arg vm_st) {
     auto vm_e = cnstr_get(vm_st, 0);
-    auto env = to_environment(vm_e);
+    environment env(vm_e, true);
     auto filename = string_to_std(vm_filename);
     std::stringstream in;
     auto ngen = to_name_generator(cnstr_get(vm_st, 1));
@@ -530,14 +529,14 @@ extern "C" obj_res lean_elaborator_elaborate_command(b_obj_arg vm_filename, obj_
             }
 
             object * args[] = {
-                    to_lean_environment(p.env()),
-                    to_obj(s->m_ngen).steal(),
-                    vm_lds.steal(),
-                    vm_eds.steal(),
-                    cnstr_get(vm_st, 4),
-                    cnstr_get(vm_st, 5),
-                    cnstr_get(vm_st, 6),
-                    cnstr_get(vm_st, 7)
+                p.env().get_obj_arg(),
+                to_obj(s->m_ngen).steal(),
+                vm_lds.steal(),
+                vm_eds.steal(),
+                cnstr_get(vm_st, 4),
+                cnstr_get(vm_st, 5),
+                cnstr_get(vm_st, 6),
+                cnstr_get(vm_st, 7)
             };
             inc(cnstr_get(vm_st, 4));
             inc(cnstr_get(vm_st, 5));
diff --git a/src/frontends/lean/lean_environment.cpp b/src/frontends/lean/lean_environment.cpp
deleted file mode 100644
index c0978b8112..0000000000
--- a/src/frontends/lean/lean_environment.cpp
+++ /dev/null
@@ -1,65 +0,0 @@
-/*
-Copyright (c) 2018 Sebastian Ullrich. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Authors: Sebastian Ullrich
-
-Lean interface to the kernel environment type and extensions
-*/
-
-#include <string>
-#include <iostream>
-#include "library/replace_visitor.h"
-#include "library/placeholder.h"
-#include "library/explicit.h"
-#include "library/annotation.h"
-#include "util/timeit.h"
-#include "library/locals.h"
-#include "library/trace.h"
-#include "frontends/lean/elaborator.h"
-#include "frontends/lean/parser.h"
-#include "frontends/lean/decl_cmds.h"
-#include "frontends/lean/definition_cmds.h"
-#include "frontends/lean/brackets.h"
-#include "frontends/lean/choice.h"
-#include "frontends/lean/inductive_cmds.h"
-#include "frontends/lean/structure_cmd.h"
-#include "frontends/lean/util.h"
-#include "frontends/lean/pp.h"
-#include "frontends/lean/simple_pos_info_provider.h"
-
-namespace lean {
-void env_finalizer(void * env) {
-    delete static_cast<environment*>(env);
-}
-
-void env_foreach(void * /* env */, b_obj_arg /* fn */) {
-    // TODO(leo, kha)
-    throw exception("unimplemented: sharing `environment` across threads");
-}
-
-static external_object_class * g_env_class = nullptr;
-
-environment const & to_environment(b_obj_arg o) {
-    lean_assert(external_class(o) == g_env_class);
-    return *static_cast<environment *>(external_data(o));
-}
-
-obj_res to_lean_environment(environment const & env) {
-    return alloc_external(g_env_class, new environment(env));
-}
-
-extern "C" obj_res lean_environment_mk_empty(b_obj_arg) {
-    return to_lean_environment(environment());
-}
-
-extern "C" uint8 lean_environment_contains(b_obj_arg lean_environment, b_obj_arg vm_n) {
-    return static_cast<uint8>(static_cast<bool>(to_environment(lean_environment).find(name(vm_n, true))));
-}
-
-void initialize_lean_environment() {
-    g_env_class = register_external_object_class(env_finalizer, env_foreach);
-}
-void finalize_lean_environment() {
-}
-}
diff --git a/src/frontends/lean/lean_environment.h b/src/frontends/lean/lean_environment.h
deleted file mode 100644
index af64d319d4..0000000000
--- a/src/frontends/lean/lean_environment.h
+++ /dev/null
@@ -1,17 +0,0 @@
-/*
-Copyright (c) 2018 Sebastian Ullrich. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Authors: Sebastian Ullrich
-
-Lean interface to the kernel environment type and extensions
-*/
-#pragma once
-#include "kernel/environment.h"
-
-namespace lean {
-environment const & to_environment(b_obj_arg o);
-obj_res to_lean_environment(environment const & env);
-void initialize_lean_environment();
-void finalize_lean_environment();
-}
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index dae2b08405..be2f51c0e5 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -42,11 +42,11 @@ environment::environment(unsigned trust_lvl):
 }
 
 unsigned environment::trust_lvl() const {
-    return environment_trust_level_core(object_ref::get());
+    return environment_trust_level_core(get_obj_arg());
 }
 
 bool environment::is_quot_initialized() const {
-    return environment_quot_init_core(object_ref::get()) != 0;
+    return environment_quot_init_core(get_obj_arg()) != 0;
 }
 
 void environment::mark_quot_initialized() {
@@ -61,11 +61,11 @@ template<typename T> optional<T> to_optional(obj_arg o) {
 }
 
 optional<constant_info> environment::find(name const & n) const {
-    return to_optional<constant_info>(environment_find_core(object_ref::get(), n.get()));
+    return to_optional<constant_info>(environment_find_core(get_obj_arg(), n.get_obj_arg()));
 }
 
 constant_info environment::get(name const & n) const {
-    object * o = environment_find_core(object_ref::get(), n.get());
+    object * o = environment_find_core(get_obj_arg(), n.get_obj_arg());
     if (is_scalar(o))
         throw unknown_constant_exception(*this, n);
     constant_info r(cnstr_get(o, 0), true);
@@ -127,11 +127,11 @@ static void check_constant_val(environment const & env, constant_val const & v,
 }
 
 void environment::add_core(constant_info const & info) {
-    m_obj = environment_add_core(m_obj, info.get());
+    m_obj = environment_add_core(m_obj, info.get_obj_arg());
 }
 
 environment environment::add(constant_info const & info) const {
-    return environment(environment_add_core(object_ref::get(), info.get()));
+    return environment(environment_add_core(get_obj_arg(), info.get_obj_arg()));
 }
 
 environment environment::add_axiom(declaration const & d, bool check) const {
@@ -275,7 +275,7 @@ unsigned environment::register_extension(environment_extension * initial) {
 }
 
 environment_extension const & environment::get_extension(unsigned id) const {
-    object * r = get_extension_core(object_ref::get(), box(id));
+    object * r = get_extension_core(get_obj_arg(), box(id));
     if (is_scalar(r)) { throw exception("invalid extension id"); }
     object * ext = cnstr_get(r, 0);
     dec(r);
@@ -283,7 +283,7 @@ environment_extension const & environment::get_extension(unsigned id) const {
 }
 
 environment environment::update(unsigned id, environment_extension * ext) const {
-    object * r = set_extension_core(object_ref::get(), box(id), to_object(ext));
+    object * r = set_extension_core(get_obj_arg(), box(id), to_object(ext));
     if (is_scalar(r)) { throw exception("invalid extension id"); }
     environment env(cnstr_get(r, 0), true);
     dec(r);
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 0d95921995..46890679ec 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -39,7 +39,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/pp.h"
 #include "frontends/lean/json.h"
 #include "frontends/lean/util.h"
-#include "frontends/lean/lean_environment.h"
 #include "library/trace.h"
 #include "init/init.h"
 #include "frontends/lean/simple_pos_info_provider.h"
@@ -506,14 +505,14 @@ int main(int argc, char ** argv) {
             scope_message_log scope_log(l);
             // res : estate.result io.error io.world (prod (list syntax) environment)
             object_ref res { lean_process_file(mk_string(mod_fn), mk_string(contents), static_cast<uint8>(json_output),
-                                               to_lean_environment(env), io_mk_world()) };
+                                               env.get_obj_arg(), io_mk_world()) };
             if (io_result_is_error(res.raw())) {
                 // estate.result.error _
                 ok = false;
             } else {
                 // estate.result.ok (prod (list syntax) environment) io.world
                 ok = true;
-                env = to_environment(cnstr_get(io_result_get_value(res.raw()), 1));
+                env = environment(cnstr_get(io_result_get_value(res.raw()), 1), true);
             }
         } else {
             message_log l;
diff --git a/src/stage0/init/lean/elaborator.cpp b/src/stage0/init/lean/elaborator.cpp
index 264f3a2de0..706d14cfbf 100644
--- a/src/stage0/init/lean/elaborator.cpp
+++ b/src/stage0/init/lean/elaborator.cpp
@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.elaborator
-// Imports: init.lean.parser.module init.lean.expander init.lean.expr init.lean.options
+// Imports: init.lean.parser.module init.lean.expander init.lean.expr init.lean.options init.lean.environment
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -50,7 +50,6 @@ obj* l_List_map___main___at_Lean_Elaborator_toPexpr___main___spec__2(obj*);
 obj* l_Lean_Elaborator_processCommand(obj*, obj*, obj*);
 obj* l_Lean_Elaborator_toLevel___main___closed__1;
 obj* l_List_mfilter___main___at_Lean_Elaborator_variables_elaborate___spec__1___boxed(obj*, obj*, obj*, obj*);
-obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2___closed__1;
 obj* l_Lean_Format_pretty(obj*, obj*);
 obj* l_Lean_Elaborator_mkNotationKind___rarg___closed__1;
 obj* l_Lean_Elaborator_ElaboratorM_MonadExcept;
@@ -60,6 +59,7 @@ obj* l_RBNode_find___main___at_Lean_Elaborator_processCommand___spec__3___boxed(
 obj* l_Lean_Elaborator_toPexpr___main___closed__21;
 obj* l_Lean_Elaborator_matchSpec(obj*, obj*);
 obj* l_Lean_Elaborator_matchOpenSpec(obj*, obj*);
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__2___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_RBTree_toList___at_Lean_Elaborator_oldElabCommand___spec__1(obj*);
 obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__6___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_elaboratorInh(obj*, obj*, obj*, obj*);
@@ -69,7 +69,6 @@ obj* l_List_mfoldl___main___at_Lean_Elaborator_CommandParserConfig_registerNotat
 obj* l_List_foldl___main___at_Lean_Elaborator_toPexpr___main___spec__16(obj*, obj*);
 extern obj* l_Lean_Parser_command_namespace;
 extern obj* l_Lean_Parser_Level_trailing_HasView;
-obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_List_lengthAux___main___rarg(obj*, obj*);
 extern obj* l_Lean_Parser_Level_leading_HasView_x_27___lambda__1___closed__5;
 obj* l_List_mfoldl___main___at_Lean_Elaborator_CommandParserConfig_registerNotationTokens___spec__1(obj*, obj*);
@@ -81,19 +80,19 @@ obj* l_Lean_Elaborator_toPexpr___main___closed__22;
 obj* l_List_mmap___main___at_Lean_Elaborator_attribute_elaborate___spec__1___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_ElaboratorM_MonadState;
 obj* l_Lean_Elaborator_elaborators;
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__3___closed__2;
 obj* l_StateT_Monad___rarg(obj*);
 extern "C" obj* lean_expr_mk_pi(obj*, uint8, obj*, obj*);
 obj* l_Lean_Elaborator_resolveContext___main___closed__1;
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__3___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_section_elaborate(obj*, obj*, obj*, obj*);
-obj* l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__1___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_variables_elaborate___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_reserveNotation_elaborate___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_processCommand___lambda__1___closed__2;
+obj* l_Lean_Elaborator_declaration_elaborate___closed__3;
 obj* l_Lean_Elaborator_variables_elaborate(obj*, obj*, obj*, obj*);
+obj* l_ReaderT_bind___at_Lean_Elaborator_declaration_elaborate___spec__1(obj*, obj*);
 obj* l_Lean_Elaborator_oldElabCommand(obj*, obj*, obj*, obj*, obj*);
 uint8 l_Lean_Elaborator_isOpenNamespace(obj*, obj*);
+extern obj* l_Lean_SMap_insert___main___at_Lean_Environment_add___spec__1___closed__1;
 obj* l_Lean_Elaborator_toPexpr___main___closed__37;
 extern "C" obj* level_mk_mvar(obj*);
 obj* l_List_foldl___main___at_Lean_Elaborator_include_elaborate___spec__1(obj*, obj*);
@@ -106,7 +105,6 @@ obj* l_List_foldl___main___at_Lean_Parser_Term_mkApp___spec__1(obj*, obj*);
 obj* l_List_reverse___rarg(obj*);
 obj* l_Lean_Elaborator_toPexpr___main___closed__9;
 extern obj* l_Lean_Parser_command_attribute;
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_TokenMap_insert___rarg(obj*, obj*, obj*);
 obj* l_RBNode_insert___rarg(obj*, obj*, obj*, obj*);
 obj* l_List_mmap___main___at_Lean_Elaborator_attrsToPexpr___spec__1(obj*, obj*, obj*, obj*);
@@ -124,7 +122,6 @@ obj* l_Lean_KVMap_setNat(obj*, obj*, obj*);
 obj* l_Lean_Elaborator_toPexpr___main___closed__4;
 obj* l_Lean_Elaborator_declModifiersToPexpr___closed__2;
 obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__17(obj*, obj*, obj*, obj*);
-obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__5___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_List_foldl___main___at_Lean_Elaborator_mangleIdent___spec__1(obj*, obj*);
 obj* l_Lean_Parser_Combinators_node___at_Lean_Parser_command_NotationSpec_precedenceLit_Parser___spec__1(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_inferModToPexpr___closed__3;
@@ -137,6 +134,7 @@ obj* l_Lean_Expr_mkCapp(obj*, obj*);
 obj* l_Lean_Elaborator_end_elaborate___closed__1;
 obj* l_Lean_Elaborator_toPexpr___main___closed__19;
 obj* l_Lean_Expander_error___at_Lean_Elaborator_processCommand___spec__1___boxed(obj*);
+obj* l_Lean_Elaborator_declaration_elaborate___closed__1;
 obj* l_Lean_Elaborator_OrderedRBMap_ofList___boxed(obj*, obj*);
 obj* l_Lean_Parser_Term_simpleBinder_View_toBinderInfo___main(obj*);
 obj* l_Lean_Elaborator_toPexpr___main___closed__31;
@@ -162,6 +160,7 @@ obj* l_Lean_Elaborator_check_elaborate(obj*, obj*, obj*, obj*);
 obj* l_List_foldl___main___at_Lean_Elaborator_OrderedRBMap_ofList___spec__1___boxed(obj*, obj*);
 obj* l_Lean_Elaborator_OrderedRBMap_empty___rarg___boxed(obj*);
 obj* l_monadStateTrans___rarg(obj*, obj*);
+obj* l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__5(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_namesToPexpr(obj*);
 obj* l_Lean_Elaborator_OrderedRBMap_insert___boxed(obj*, obj*);
 obj* l_Lean_Name_quickLt___boxed(obj*, obj*);
@@ -169,7 +168,6 @@ obj* l_Lean_Elaborator_toLevel___main___closed__4;
 obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__3(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_notation_elaborate___closed__1;
 obj* l_Lean_Elaborator_mkState___closed__4;
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__2(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_RBTree_ofList___main___at_Lean_Elaborator_oldElabCommand___spec__3(obj*);
 obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__15___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Level_ofNat___main(obj*);
@@ -186,6 +184,7 @@ extern obj* l_Lean_Parser_command_export_HasView;
 obj* l_List_mmap___main___at_Lean_Elaborator_attribute_elaborate___spec__1(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_resolveContext___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_inferModToPexpr___closed__1;
+extern obj* l_Lean_Parser_command_declaration_HasView;
 obj* l_Lean_Elaborator_notation_elaborateAux(obj*, obj*, obj*, obj*);
 obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__6(obj*, obj*, obj*, obj*, obj*);
 extern obj* l_Lean_Parser_command_variables_HasView;
@@ -201,6 +200,7 @@ obj* l_Lean_Elaborator_simpleBindersToPexpr___boxed(obj*, obj*, obj*, obj*);
 obj* l_List_foldl___main___at_Lean_Elaborator_elabDefLike___spec__3(obj*, obj*);
 obj* l_Lean_Parser_Syntax_asNode___main(obj*);
 obj* l_Lean_Elaborator_toPexpr___main___closed__44;
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_levelAdd___main(obj*, obj*);
 extern obj* l_Lean_Parser_command_end_HasView;
 obj* l_Lean_Elaborator_attribute_elaborate___closed__2;
@@ -218,7 +218,6 @@ obj* l_Lean_Elaborator_toPexpr___main___closed__27;
 obj* l_ReaderT_lift___rarg___boxed(obj*, obj*);
 obj* l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__3(obj*, obj*, obj*);
 obj* l_Lean_Elaborator_preresolve___boxed(obj*, obj*, obj*, obj*);
-obj* l_ReaderT_bind___at_Lean_Elaborator_Declaration_elaborate___spec__1(obj*, obj*);
 obj* l_Lean_Elaborator_Module_header_elaborate(obj*, obj*, obj*, obj*);
 extern "C" obj* lean_expr_mk_const(obj*, obj*);
 obj* l_Lean_Elaborator_toLevel___boxed(obj*, obj*, obj*, obj*);
@@ -243,20 +242,22 @@ obj* l_List_mfoldl___main___at_Lean_Elaborator_updateParserConfig___spec__2___bo
 obj* l_Lean_Elaborator_declModifiersToPexpr(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_toPexpr___main___closed__29;
 extern obj* l_Lean_Parser_Term_structInstItem_HasView;
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__3___closed__1;
 extern obj* l_Lean_Parser_command_setOption_HasView;
 obj* l_Lean_Elaborator_Expr_mkAnnotation___closed__1;
 obj* l_Lean_Elaborator_ElaboratorM_Lean_Parser_MonadRec;
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_toPexpr(obj*, obj*, obj*, obj*);
+obj* l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_List_map___main___at_Lean_Elaborator_elabDefLike___spec__2(obj*);
-obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__4___boxed(obj*, obj*, obj*, obj*);
 namespace lean {
 obj* string_append(obj*, obj*);
 }
 obj* l_List_mmap___main___at_Lean_Elaborator_CommandParserConfig_registerNotationParser___spec__2___closed__2;
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_registerNotationMacro(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_toPexpr___main___closed__20;
 extern obj* l_Lean_Parser_command_initQuot;
+obj* l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__5___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_KVMap_setName(obj*, obj*, obj*);
 extern obj* l_Lean_Parser_command_open_HasView;
 obj* l_Lean_Elaborator_inferModToPexpr___boxed(obj*);
@@ -273,7 +274,6 @@ uint8 nat_dec_lt(obj*, obj*);
 }
 extern obj* l_Lean_Parser_command_include_HasView;
 obj* l_List_map___main___at_Lean_Elaborator_mkEqns___spec__1___closed__1;
-obj* l_Lean_Elaborator_Declaration_elaborate___closed__3;
 obj* l_Lean_Elaborator_end_elaborate___closed__3;
 obj* l_Lean_Elaborator_toPexpr___main___closed__33;
 obj* l_Lean_Elaborator_notation_elaborate___boxed(obj*, obj*, obj*, obj*);
@@ -282,6 +282,7 @@ obj* l_Lean_Elaborator_toLevel(obj*, obj*, obj*, obj*);
 obj* l_RBNode_insert___at_Lean_Expander_builtinTransformers___spec__1(obj*, obj*, obj*);
 obj* l_Lean_Elaborator_mkEqns___closed__1;
 obj* l_Lean_Parser_Syntax_getPos(obj*);
+obj* l_ReaderT_bind___at_Lean_Elaborator_declaration_elaborate___spec__1___boxed(obj*, obj*);
 extern obj* l_Lean_Expander_builtinTransformers;
 obj* l_Lean_Expander_error___at_Lean_Elaborator_currentScope___spec__1___boxed(obj*);
 obj* l_Lean_Elaborator_declModifiersToPexpr___closed__4;
@@ -311,7 +312,7 @@ namespace lean {
 obj* nat_add(obj*, obj*);
 }
 obj* l_Lean_Elaborator_matchPrecedence___main___boxed(obj*, obj*);
-obj* l_ReaderT_bind___at_Lean_Elaborator_Declaration_elaborate___spec__1___rarg(obj*, obj*, obj*, obj*, obj*);
+obj* l_Lean_Elaborator_declaration_elaborate___closed__2;
 obj* l_RBNode_insert___at_Lean_Elaborator_elaborators___spec__1(obj*, obj*, obj*);
 extern obj* l_Lean_Parser_Module_eoi;
 obj* l_Lean_Elaborator_attrsToPexpr(obj*, obj*, obj*, obj*);
@@ -324,7 +325,6 @@ uint8 l_List_foldr___main___at_Lean_Elaborator_notation_elaborate___spec__1(uint
 obj* l_Lean_Elaborator_inferModToPexpr(obj*);
 obj* l_Lean_Elaborator_Expr_mkAnnotation(obj*, obj*);
 obj* l_StateT_MonadExcept___rarg(obj*, obj*, obj*);
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_section_elaborate___closed__1;
 obj* l_Lean_Elaborator_currentScope___closed__1;
 uint8 l_RBNode_isRed___main___rarg(obj*);
@@ -332,6 +332,7 @@ obj* l_Lean_Elaborator_OrderedRBMap_ofList(obj*, obj*);
 obj* l_List_mmap___main___at_Lean_Elaborator_CommandParserConfig_registerNotationParser___spec__2(obj*);
 obj* l_Lean_Elaborator_setOption_elaborate___lambda__1(obj*, obj*);
 obj* l_Lean_Elaborator_noKind_elaborate___closed__1;
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__3___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_CommandParserConfig_registerNotationTokens(obj*, obj*);
 obj* l_Lean_Elaborator_updateParserConfig___boxed(obj*, obj*, obj*);
 obj* l_Lean_Elaborator_toPexpr___main___closed__11;
@@ -343,16 +344,12 @@ obj* l_Lean_Elaborator_OrderedRBMap_find___boxed(obj*, obj*);
 extern "C" obj* level_mk_imax(obj*, obj*);
 obj* l_Lean_Elaborator_section_elaborate___boxed(obj*, obj*, obj*, obj*);
 uint8 l_List_foldr___main___at_Lean_Elaborator_isOpenNamespace___main___spec__2(obj*, uint8, obj*);
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__2___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
-extern obj* l_Lean_Parser_command_Declaration;
 obj* l_Lean_Parser_Combinators_node___at_Lean_Parser_Term_sortApp_Parser_Lean_Parser_HasTokens___spec__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_universe_elaborate___boxed(obj*, obj*, obj*, obj*);
 obj* l_List_foldr___main___at_Lean_Elaborator_toLevel___main___spec__3(obj*, obj*);
-obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__5(obj*, obj*, obj*, obj*, obj*, obj*);
 extern obj* l_Lean_Parser_Level_trailing_HasView_x_27___lambda__1___closed__2;
 obj* l_Lean_Elaborator_OrderedRBMap_find(obj*, obj*);
 obj* l_Lean_Elaborator_preresolve(obj*, obj*, obj*, obj*);
-obj* l_Lean_Elaborator_Declaration_elaborate(obj*, obj*, obj*, obj*);
 extern obj* l_Lean_Expander_expandBracketedBinder___main___closed__4;
 obj* l_Lean_Elaborator_toPexpr___main___closed__13;
 obj* l_Lean_Elaborator_processCommand___lambda__1___closed__1;
@@ -361,7 +358,6 @@ namespace lean {
 uint8 string_dec_eq(obj*, obj*);
 }
 obj* l_Lean_Elaborator_processCommand___closed__1;
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__3___closed__1;
 obj* l_Lean_Elaborator_check_elaborate___boxed(obj*, obj*, obj*, obj*);
 extern obj* l_Lean_Parser_command_open;
 obj* l_Lean_Elaborator_OrderedRBMap_empty___boxed(obj*, obj*);
@@ -401,7 +397,6 @@ obj* l_Lean_Elaborator_mkEqns(obj*, obj*);
 obj* l_Lean_Elaborator_namespace_elaborate___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_isOpenNamespace___boxed(obj*, obj*);
 obj* l_String_trim(obj*);
-obj* l_Lean_Elaborator_toLevel___main___closed__5;
 extern obj* l_Lean_Parser_command_universe;
 obj* l_List_filterMap___main___at_Lean_Elaborator_resolveContext___main___spec__2(obj*, obj*);
 obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__10___boxed(obj*, obj*, obj*, obj*, obj*);
@@ -413,7 +408,6 @@ extern "C" obj* level_mk_succ(obj*);
 obj* l_Lean_Elaborator_levelGetAppArgs___main___closed__1;
 obj* l_Lean_Elaborator_toPexpr___main___closed__43;
 extern obj* l_Lean_Expander_bindingAnnotationUpdate;
-obj* l_ReaderT_bind___at_Lean_Elaborator_Declaration_elaborate___spec__1___boxed(obj*, obj*);
 obj* l_Lean_Elaborator_toPexpr___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_levelAdd___boxed(obj*, obj*);
 extern obj* l_Lean_Parser_command_namespace_HasView;
@@ -421,9 +415,11 @@ obj* l_Lean_Elaborator_setOption_elaborate___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_levelGetAppArgs(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_elabDefLike___closed__1;
 obj* l_Lean_Elaborator_levelGetAppArgs___main(obj*, obj*, obj*, obj*);
+extern obj* l_Lean_Parser_command_declaration;
 obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__13(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_levelGetAppArgs___main___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_namespace_elaborate___closed__1;
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__2(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__4___boxed(obj*, obj*, obj*);
 obj* l_Lean_Elaborator_mkState___closed__1;
 obj* l_List_mmap___main___at_Lean_Elaborator_toLevel___main___spec__1___boxed(obj*, obj*, obj*, obj*);
@@ -443,18 +439,17 @@ extern obj* l_Lean_Parser_Term_anonymousConstructor_HasView;
 obj* l_Lean_Elaborator_end_elaborate(obj*, obj*, obj*, obj*);
 obj* l_List_map___main___at_Lean_Elaborator_CommandParserConfig_registerNotationParser___spec__5(obj*);
 obj* l_Lean_Elaborator_elaboratorConfigCoeFrontendConfig(obj*);
-obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__4(obj*, obj*, obj*, obj*);
-obj* l_Lean_Elaborator_Declaration_elaborate___closed__4;
 obj* l_List_mmap___main___at_Lean_Elaborator_preresolve___main___spec__1(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_oldElabCommand___boxed(obj*, obj*, obj*, obj*, obj*);
-obj* l_Lean_Elaborator_Declaration_elaborate___closed__5;
 obj* l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__6(obj*, obj*, obj*);
 obj* l_Lean_Elaborator_toPexpr___main___closed__24;
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__3___closed__2;
 uint8 l_List_decidableMem___main___at_Lean_Elaborator_isOpenNamespace___main___spec__1(obj*, obj*);
 obj* l_Lean_Elaborator_initQuot_elaborate___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_number_View_ofNat(obj*);
-obj* l_Lean_environment_contains___boxed(obj*, obj*);
+obj* l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2(obj*, obj*, obj*, obj*, obj*);
 extern obj* l_Lean_Parser_Term_borrowed_HasView;
+obj* l_Lean_Elaborator_declaration_elaborate(obj*, obj*, obj*, obj*);
 obj* l_Lean_Expander_error___at_Lean_Elaborator_processCommand___spec__1___rarg___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_toPexpr___main___closed__26;
 obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__9(obj*, obj*, obj*, obj*, obj*);
@@ -465,8 +460,8 @@ obj* l_Lean_KVMap_setString(obj*, obj*, obj*);
 obj* l_Lean_Elaborator_CommandParserConfig_registerNotationParser___closed__1;
 obj* l_Lean_Parser_RecT_recurse___rarg(obj*, obj*);
 obj* l_Lean_Elaborator_notation_elaborate___lambda__1(obj*, obj*);
+obj* l_Lean_Elaborator_declaration_elaborate___closed__4;
 obj* l_Lean_Elaborator_elabDefLike___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
-extern "C" uint8 lean_environment_contains(obj*, obj*);
 obj* l_ExceptT_Monad___rarg(obj*);
 extern obj* l_Lean_Parser_number_HasView_x_27___lambda__1___closed__6;
 obj* l_Lean_Elaborator_preresolve___main(obj*, obj*, obj*, obj*);
@@ -479,6 +474,7 @@ obj* l_Lean_Elaborator_variables_elaborate___closed__2;
 obj* l_Lean_Elaborator_processCommand___lambda__1(obj*, obj*, obj*, obj*);
 obj* l_Lean_KVMap_insertCore___main(obj*, obj*, obj*);
 obj* l_Lean_Elaborator_toPexpr___main___closed__16;
+obj* l_ReaderT_bind___at_Lean_Elaborator_declaration_elaborate___spec__1___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_toPexpr___main___closed__35;
 obj* l_Lean_Elaborator_toPexpr___main___closed__7;
 namespace lean {
@@ -492,9 +488,11 @@ obj* l_Lean_Elaborator_updateParserConfig(obj*, obj*, obj*);
 obj* l_Lean_Elaborator_ElaboratorM_MonadReader;
 obj* l_Lean_Elaborator_toPexpr___main___closed__41;
 obj* l_Lean_Elaborator_toPexpr___main___closed__25;
+uint8 l_Lean_Environment_contains(obj*, obj*);
 obj* l_Lean_Elaborator_attribute_elaborate___closed__1;
 obj* l_RBNode_find___main___at_Lean_Elaborator_processCommand___spec__3(obj*, obj*);
 obj* l_Lean_Elaborator_matchPrecedence___boxed(obj*, obj*);
+obj* l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2___closed__1;
 obj* l_List_map___main___at_Lean_Elaborator_mkEqns___spec__1(obj*, obj*);
 extern "C" obj* lean_expr_mk_lambda(obj*, uint8, obj*, obj*);
 obj* l_Lean_Elaborator_end_elaborate___boxed(obj*, obj*, obj*, obj*);
@@ -514,7 +512,6 @@ obj* l_Lean_Elaborator_levelAdd(obj*, obj*);
 obj* l_Lean_Elaborator_eoi_elaborate(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_noKind_elaborate(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_Module_header_elaborate___boxed(obj*, obj*, obj*, obj*);
-obj* l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__6___boxed(obj*, obj*, obj*);
 obj* l_Lean_FileMap_toPosition(obj*, obj*);
 obj* l_List_foldr___main___at_Lean_Elaborator_toLevel___main___spec__2(obj*, obj*);
 extern obj* l_Lean_Parser_stringLit_HasView;
@@ -523,6 +520,7 @@ obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__11___boxed(o
 obj* l_Lean_Elaborator_currentScope(obj*, obj*, obj*);
 obj* l_Option_toMonad___main___at_Lean_Elaborator_CommandParserConfig_registerNotationParser___spec__1___boxed(obj*);
 extern obj* l_Lean_Parser_Term_inaccessible_HasView;
+obj* l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__4___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_precToNat___main(obj*);
 obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__1___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_include_elaborate___boxed(obj*, obj*, obj*, obj*);
@@ -538,20 +536,16 @@ obj* l_Lean_Elaborator_elaboratorConfigCoeFrontendConfig___boxed(obj*);
 obj* l_Lean_Expr_local___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_Substring_ofString(obj*);
 obj* l_List_mmap___main___at_Lean_Elaborator_preresolve___main___spec__1___boxed(obj*, obj*, obj*, obj*);
-obj* l_Lean_Elaborator_Declaration_elaborate___closed__1;
-extern obj* l_Lean_Parser_command_Declaration_HasView;
 obj* l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__4(obj*, obj*, obj*);
-obj* l_List_map___main___at_Lean_Elaborator_Declaration_elaborate___spec__3(obj*);
 extern obj* l_Lean_Expander_noExpansion___closed__1;
 extern obj* l_Lean_Parser_Term_sort_HasView;
 obj* l_Lean_Elaborator_resolveContext(obj*, obj*, obj*, obj*);
-obj* l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__3___boxed(obj*, obj*, obj*);
 obj* l_Lean_Elaborator_toPexpr___main___closed__23;
 obj* l_List_mmap___main___at_Lean_Elaborator_attribute_elaborate___spec__1___closed__1;
 obj* l_ReaderT_lift___boxed(obj*, obj*, obj*, obj*);
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_List_foldr___main___at_Lean_Elaborator_toLevel___main___spec__3___boxed(obj*, obj*);
 extern obj* l_Lean_Parser_identUnivs_HasView;
-obj* l_Lean_Elaborator_Declaration_elaborate___closed__2;
 obj* l_Lean_Expander_error___at_Lean_Elaborator_currentScope___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_notation_elaborate___closed__2;
 extern obj* l_Lean_Parser_command_reserveNotation;
@@ -562,6 +556,7 @@ obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__17___boxed(o
 obj* l_List_foldr___main___at_Lean_Elaborator_toPexpr___main___spec__7___boxed(obj*, obj*);
 obj* l_List_foldr___main___at_Lean_Elaborator_notation_elaborate___spec__1___boxed(obj*, obj*);
 obj* l_List_mfilter___main___at_Lean_Elaborator_variables_elaborate___spec__1___lambda__1(obj*, uint8, obj*, obj*);
+obj* l_List_map___main___at_Lean_Elaborator_declaration_elaborate___spec__3(obj*);
 uint8 l_Lean_Elaborator_matchPrecedence___main(obj*, obj*);
 obj* l_Lean_Elaborator_attrsToPexpr___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_mkState___closed__2;
@@ -569,7 +564,6 @@ obj* l_Lean_Elaborator_initQuot_elaborate___closed__1;
 obj* l_StateT_MonadState___rarg(obj*);
 obj* l_List_decidableMem___main___at_Lean_Elaborator_isOpenNamespace___main___spec__1___boxed(obj*, obj*);
 extern obj* l_List_mmap___main___at_Lean_Parser_Syntax_reprint___main___spec__1___closed__1;
-obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2(obj*, obj*, obj*, obj*, obj*);
 obj* l_List_foldr___main___at_Lean_Elaborator_toPexpr___main___spec__7(obj*, obj*);
 obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__14(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elaborator_universe_elaborate(obj*, obj*, obj*, obj*);
@@ -582,6 +576,8 @@ extern obj* l_Lean_Parser_Term_let_HasView;
 obj* l_Lean_Parser_number_View_toNat___main(obj*);
 extern "C" obj* level_mk_max(obj*, obj*);
 obj* l_Lean_Parser_Term_binders_Parser(obj*, obj*, obj*, obj*, obj*);
+obj* l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__4(obj*, obj*, obj*, obj*);
+obj* l_Lean_Elaborator_declaration_elaborate___closed__5;
 extern obj* l_Lean_Parser_Term_pi_HasView;
 obj* l_Lean_Expander_error___at_Lean_Elaborator_processCommand___spec__1___rarg(obj*, obj*, obj*, obj*);
 obj* l_List_mmap___main___at_Lean_Elaborator_matchSpec___spec__1(obj*);
@@ -594,17 +590,6 @@ obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__12(obj*, obj
 extern obj* l_String_splitAux___main___closed__1;
 obj* l_Lean_Elaborator_locally(obj*, obj*, obj*, obj*);
 extern obj* l_Lean_Parser_command_include;
-obj* l_Lean_environment_contains___boxed(obj* x_0, obj* x_1) {
-_start:
-{
-uint8 x_2; obj* x_3; 
-x_2 = lean_environment_contains(x_0, x_1);
-x_3 = lean::box(x_2);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_3;
-}
-}
 obj* l_Lean_Expr_local___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
@@ -1757,14 +1742,6 @@ obj* _init_l_Lean_Elaborator_toLevel___main___closed__4() {
 _start:
 {
 obj* x_0; 
-x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Name_quickLt___boxed), 2, 0);
-return x_0;
-}
-}
-obj* _init_l_Lean_Elaborator_toLevel___main___closed__5() {
-_start:
-{
-obj* x_0; 
 x_0 = lean::mk_string("unknown universe variable '");
 return x_0;
 }
@@ -2445,7 +2422,7 @@ x_291 = l_Lean_Elaborator_mangleIdent(x_288);
 x_292 = lean::cnstr_get(x_39, 3);
 lean::inc(x_292);
 lean::dec(x_39);
-x_295 = l_Lean_Elaborator_toLevel___main___closed__4;
+x_295 = l_Lean_SMap_insert___main___at_Lean_Environment_add___spec__1___closed__1;
 lean::inc(x_291);
 x_297 = l_Lean_Elaborator_OrderedRBMap_find___rarg(x_295, x_292, x_291);
 if (lean::obj_tag(x_297) == 0)
@@ -2461,7 +2438,7 @@ if (lean::is_scalar(x_64)) {
 lean::cnstr_set(x_300, 0, x_0);
 x_301 = l_Lean_Name_toString___closed__1;
 x_302 = l_Lean_Name_toStringWithSep___main(x_301, x_291);
-x_303 = l_Lean_Elaborator_toLevel___main___closed__5;
+x_303 = l_Lean_Elaborator_toLevel___main___closed__4;
 x_304 = lean::string_append(x_303, x_302);
 lean::dec(x_302);
 x_306 = l_Char_HasRepr___closed__1;
@@ -12329,7 +12306,7 @@ if (lean::is_exclusive(x_1)) {
 }
 x_13 = lean::cnstr_get(x_0, 2);
 lean::inc(x_13);
-x_15 = l_Lean_Elaborator_toLevel___main___closed__4;
+x_15 = l_Lean_SMap_insert___main___at_Lean_Environment_add___spec__1___closed__1;
 x_16 = l_Lean_Elaborator_OrderedRBMap_ofList___rarg(x_15, x_13);
 x_17 = lean::cnstr_get(x_0, 3);
 lean::inc(x_17);
@@ -14330,7 +14307,7 @@ lean::inc(x_4);
 lean::dec(x_1);
 lean::inc(x_2);
 x_8 = level_mk_param(x_2);
-x_9 = l_Lean_Elaborator_toLevel___main___closed__4;
+x_9 = l_Lean_SMap_insert___main___at_Lean_Environment_add___spec__1___closed__1;
 x_10 = l_Lean_Elaborator_OrderedRBMap_insert___rarg(x_9, x_0, x_2, x_8);
 x_0 = x_10;
 x_1 = x_4;
@@ -14953,7 +14930,7 @@ lean::dec(x_0);
 return x_1;
 }
 }
-obj* l_ReaderT_bind___at_Lean_Elaborator_Declaration_elaborate___spec__1___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+obj* l_ReaderT_bind___at_Lean_Elaborator_declaration_elaborate___spec__1___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
 obj* x_7; 
@@ -14998,23 +14975,23 @@ return x_23;
 }
 }
 }
-obj* l_ReaderT_bind___at_Lean_Elaborator_Declaration_elaborate___spec__1(obj* x_0, obj* x_1) {
+obj* l_ReaderT_bind___at_Lean_Elaborator_declaration_elaborate___spec__1(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; 
-x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_ReaderT_bind___at_Lean_Elaborator_Declaration_elaborate___spec__1___rarg), 5, 0);
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_ReaderT_bind___at_Lean_Elaborator_declaration_elaborate___spec__1___rarg), 5, 0);
 return x_2;
 }
 }
-obj* _init_l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2___closed__1() {
+obj* _init_l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2___closed__1() {
 _start:
 {
 obj* x_0; 
-x_0 = lean::mk_string("Declaration.elaborate: unexpected input");
+x_0 = lean::mk_string("declaration.elaborate: unexpected input");
 return x_0;
 }
 }
-obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+obj* l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
 if (lean::obj_tag(x_1) == 0)
@@ -15132,7 +15109,7 @@ x_61 = l_Lean_Elaborator_mangleIdent(x_58);
 x_62 = 0;
 lean::inc(x_61);
 x_64 = lean_expr_local(x_61, x_61, x_53, x_62);
-x_65 = l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2(x_0, x_12, x_2, x_3, x_55);
+x_65 = l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2(x_0, x_12, x_2, x_3, x_55);
 if (lean::obj_tag(x_65) == 0)
 {
 obj* x_67; obj* x_69; obj* x_70; 
@@ -15213,7 +15190,7 @@ lean::dec(x_15);
 lean::inc(x_0);
 x_88 = lean::alloc_cnstr(1, 1, 0);
 lean::cnstr_set(x_88, 0, x_0);
-x_89 = l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2___closed__1;
+x_89 = l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2___closed__1;
 lean::inc(x_3);
 x_91 = l_Lean_Expander_error___at_Lean_Elaborator_currentScope___spec__1___rarg(x_88, x_89, x_2, x_3, x_4);
 lean::dec(x_4);
@@ -15252,7 +15229,7 @@ lean::inc(x_105);
 x_107 = lean::cnstr_get(x_102, 1);
 lean::inc(x_107);
 lean::dec(x_102);
-x_110 = l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2(x_0, x_12, x_2, x_3, x_107);
+x_110 = l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2(x_0, x_12, x_2, x_3, x_107);
 if (lean::obj_tag(x_110) == 0)
 {
 obj* x_113; obj* x_115; obj* x_116; 
@@ -15322,7 +15299,7 @@ return x_127;
 }
 }
 }
-obj* l_List_map___main___at_Lean_Elaborator_Declaration_elaborate___spec__3(obj* x_0) {
+obj* l_List_map___main___at_Lean_Elaborator_declaration_elaborate___spec__3(obj* x_0) {
 _start:
 {
 if (lean::obj_tag(x_0) == 0)
@@ -15349,7 +15326,7 @@ lean::inc(x_7);
 lean::dec(x_2);
 x_10 = l_Lean_Elaborator_inferModToPexpr(x_7);
 lean::dec(x_7);
-x_12 = l_List_map___main___at_Lean_Elaborator_Declaration_elaborate___spec__3(x_4);
+x_12 = l_List_map___main___at_Lean_Elaborator_declaration_elaborate___spec__3(x_4);
 if (lean::is_scalar(x_6)) {
  x_13 = lean::alloc_cnstr(1, 2, 0);
 } else {
@@ -15361,7 +15338,7 @@ return x_13;
 }
 }
 }
-obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__4(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+obj* l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__4(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 if (lean::obj_tag(x_0) == 0)
@@ -15429,7 +15406,7 @@ lean::inc(x_28);
 x_30 = lean::cnstr_get(x_25, 1);
 lean::inc(x_30);
 lean::dec(x_25);
-x_33 = l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__4(x_10, x_1, x_2, x_30);
+x_33 = l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__4(x_10, x_1, x_2, x_30);
 if (lean::obj_tag(x_33) == 0)
 {
 obj* x_36; obj* x_38; obj* x_39; 
@@ -15498,7 +15475,7 @@ return x_50;
 }
 }
 }
-obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__5(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
+obj* l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__5(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
 _start:
 {
 if (lean::obj_tag(x_2) == 0)
@@ -15547,7 +15524,7 @@ lean::dec(x_22);
 lean::inc(x_0);
 x_27 = lean::alloc_cnstr(1, 1, 0);
 lean::cnstr_set(x_27, 0, x_0);
-x_28 = l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2___closed__1;
+x_28 = l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2___closed__1;
 lean::inc(x_4);
 x_30 = l_Lean_Expander_error___at_Lean_Elaborator_currentScope___spec__1___rarg(x_27, x_28, x_3, x_4, x_5);
 lean::dec(x_5);
@@ -15758,7 +15735,7 @@ lean::cnstr_set(x_139, 0, x_96);
 lean::cnstr_set(x_139, 1, x_138);
 lean::inc(x_1);
 x_141 = l_Lean_Expr_mkCapp(x_1, x_139);
-x_142 = l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__5(x_0, x_1, x_14, x_3, x_4, x_132);
+x_142 = l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__5(x_0, x_1, x_14, x_3, x_4, x_132);
 if (lean::obj_tag(x_142) == 0)
 {
 obj* x_144; obj* x_146; obj* x_147; 
@@ -15823,7 +15800,7 @@ return x_158;
 }
 }
 }
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8) {
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8) {
 _start:
 {
 obj* x_9; obj* x_10; obj* x_14; 
@@ -15885,7 +15862,7 @@ return x_38;
 }
 }
 }
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__2(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8, obj* x_9, obj* x_10, obj* x_11, obj* x_12) {
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__2(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8, obj* x_9, obj* x_10, obj* x_11, obj* x_12) {
 _start:
 {
 obj* x_13; obj* x_15; 
@@ -16152,7 +16129,7 @@ lean::dec(x_138);
 lean::inc(x_11);
 lean::inc(x_5);
 lean::inc(x_4);
-x_149 = l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2(x_4, x_5, x_10, x_11, x_143);
+x_149 = l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2(x_4, x_5, x_10, x_11, x_143);
 if (lean::obj_tag(x_149) == 0)
 {
 obj* x_160; obj* x_162; obj* x_163; 
@@ -16199,7 +16176,7 @@ x_174 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_174, 0, x_172);
 lean::cnstr_set(x_174, 1, x_0);
 x_175 = l_Lean_Expr_mkCapp(x_45, x_174);
-x_176 = l_List_map___main___at_Lean_Elaborator_Declaration_elaborate___spec__3(x_5);
+x_176 = l_List_map___main___at_Lean_Elaborator_declaration_elaborate___spec__3(x_5);
 x_177 = l_Lean_Expr_mkCapp(x_45, x_176);
 lean::inc(x_0);
 x_179 = lean::alloc_cnstr(1, 2, 0);
@@ -16241,7 +16218,7 @@ return x_190;
 }
 }
 }
-obj* _init_l_Lean_Elaborator_Declaration_elaborate___lambda__3___closed__1() {
+obj* _init_l_Lean_Elaborator_declaration_elaborate___lambda__3___closed__1() {
 _start:
 {
 obj* x_0; obj* x_1; 
@@ -16250,7 +16227,7 @@ x_1 = l_Lean_Elaborator_inferModToPexpr(x_0);
 return x_1;
 }
 }
-obj* _init_l_Lean_Elaborator_Declaration_elaborate___lambda__3___closed__2() {
+obj* _init_l_Lean_Elaborator_declaration_elaborate___lambda__3___closed__2() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; 
@@ -16260,7 +16237,7 @@ x_2 = lean_name_mk_string(x_0, x_1);
 return x_2;
 }
 }
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__3(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8, obj* x_9, obj* x_10, obj* x_11, obj* x_12, obj* x_13) {
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__3(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8, obj* x_9, obj* x_10, obj* x_11, obj* x_12, obj* x_13) {
 _start:
 {
 obj* x_14; 
@@ -16462,7 +16439,7 @@ lbl_112:
 {
 obj* x_118; 
 lean::inc(x_12);
-x_118 = l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__4(x_111, x_11, x_12, x_108);
+x_118 = l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__4(x_111, x_11, x_12, x_108);
 if (lean::obj_tag(x_118) == 0)
 {
 obj* x_130; obj* x_132; obj* x_133; 
@@ -16508,11 +16485,11 @@ x_142 = l_Lean_Elaborator_mkEqns___closed__1;
 x_143 = l_Lean_Expr_mkCapp(x_142, x_137);
 lean::inc(x_12);
 lean::inc(x_3);
-x_146 = l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__5(x_3, x_142, x_4, x_11, x_12, x_139);
+x_146 = l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__5(x_3, x_142, x_4, x_11, x_12, x_139);
 if (lean::obj_tag(x_5) == 0)
 {
 obj* x_149; 
-x_149 = l_Lean_Elaborator_Declaration_elaborate___lambda__3___closed__2;
+x_149 = l_Lean_Elaborator_declaration_elaborate___lambda__3___closed__2;
 x_147 = x_149;
 goto lbl_148;
 }
@@ -16580,7 +16557,7 @@ x_181 = l_Lean_Expr_mkCapp(x_142, x_176);
 x_182 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_182, 0, x_181);
 lean::cnstr_set(x_182, 1, x_6);
-x_183 = l_Lean_Elaborator_Declaration_elaborate___lambda__3___closed__1;
+x_183 = l_Lean_Elaborator_declaration_elaborate___lambda__3___closed__1;
 x_184 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_184, 0, x_183);
 lean::cnstr_set(x_184, 1, x_182);
@@ -16708,7 +16685,7 @@ return x_240;
 }
 }
 }
-obj* _init_l_Lean_Elaborator_Declaration_elaborate___closed__1() {
+obj* _init_l_Lean_Elaborator_declaration_elaborate___closed__1() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; obj* x_4; obj* x_5; obj* x_6; 
@@ -16726,7 +16703,7 @@ lean::cnstr_set(x_6, 0, x_5);
 return x_6;
 }
 }
-obj* _init_l_Lean_Elaborator_Declaration_elaborate___closed__2() {
+obj* _init_l_Lean_Elaborator_declaration_elaborate___closed__2() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_5; obj* x_6; obj* x_7; obj* x_8; 
@@ -16749,7 +16726,7 @@ lean::cnstr_set(x_8, 1, x_0);
 return x_8;
 }
 }
-obj* _init_l_Lean_Elaborator_Declaration_elaborate___closed__3() {
+obj* _init_l_Lean_Elaborator_declaration_elaborate___closed__3() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; 
@@ -16763,7 +16740,7 @@ x_6 = l_Lean_KVMap_setName(x_5, x_2, x_4);
 return x_6;
 }
 }
-obj* _init_l_Lean_Elaborator_Declaration_elaborate___closed__4() {
+obj* _init_l_Lean_Elaborator_declaration_elaborate___closed__4() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; 
@@ -16777,7 +16754,7 @@ x_6 = l_Lean_KVMap_setName(x_5, x_2, x_4);
 return x_6;
 }
 }
-obj* _init_l_Lean_Elaborator_Declaration_elaborate___closed__5() {
+obj* _init_l_Lean_Elaborator_declaration_elaborate___closed__5() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; 
@@ -16791,11 +16768,11 @@ x_6 = l_Lean_KVMap_setName(x_5, x_2, x_4);
 return x_6;
 }
 }
-obj* l_Lean_Elaborator_Declaration_elaborate(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+obj* l_Lean_Elaborator_declaration_elaborate(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 obj* x_4; obj* x_6; obj* x_7; obj* x_11; obj* x_12; 
-x_6 = l_Lean_Parser_command_Declaration_HasView;
+x_6 = l_Lean_Parser_command_declaration_HasView;
 x_7 = lean::cnstr_get(x_6, 0);
 lean::inc(x_7);
 lean::dec(x_6);
@@ -16909,8 +16886,8 @@ obj* x_65; obj* x_68; obj* x_69; obj* x_70; obj* x_71; obj* x_72; obj* x_73;
 x_65 = lean::cnstr_get(x_47, 3);
 lean::inc(x_65);
 lean::dec(x_47);
-x_68 = l_Lean_Elaborator_Declaration_elaborate___closed__1;
-x_69 = l_Lean_Elaborator_Declaration_elaborate___closed__2;
+x_68 = l_Lean_Elaborator_declaration_elaborate___closed__1;
+x_69 = l_Lean_Elaborator_declaration_elaborate___closed__2;
 x_70 = lean::alloc_cnstr(0, 5, 0);
 lean::cnstr_set(x_70, 0, x_68);
 lean::cnstr_set(x_70, 1, x_53);
@@ -16935,7 +16912,7 @@ lean::dec(x_47);
 x_77 = lean::cnstr_get(x_56, 0);
 lean::inc(x_77);
 lean::dec(x_56);
-x_80 = l_Lean_Elaborator_Declaration_elaborate___closed__1;
+x_80 = l_Lean_Elaborator_declaration_elaborate___closed__1;
 x_81 = lean::alloc_cnstr(0, 5, 0);
 lean::cnstr_set(x_81, 0, x_80);
 lean::cnstr_set(x_81, 1, x_53);
@@ -16977,8 +16954,8 @@ lean::cnstr_set(x_100, 1, x_99);
 x_101 = lean::cnstr_get(x_85, 2);
 lean::inc(x_101);
 lean::dec(x_85);
-x_104 = l_Lean_Elaborator_Declaration_elaborate___closed__1;
-x_105 = l_Lean_Elaborator_Declaration_elaborate___closed__2;
+x_104 = l_Lean_Elaborator_declaration_elaborate___closed__1;
+x_105 = l_Lean_Elaborator_declaration_elaborate___closed__2;
 x_106 = lean::alloc_cnstr(0, 5, 0);
 lean::cnstr_set(x_106, 0, x_104);
 lean::cnstr_set(x_106, 1, x_91);
@@ -17036,14 +17013,14 @@ lean::inc(x_132);
 lean::dec(x_11);
 x_135 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elaborator_declModifiersToPexpr___boxed), 4, 1);
 lean::closure_set(x_135, 0, x_132);
-x_136 = l_Lean_Elaborator_Declaration_elaborate___closed__3;
-x_137 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elaborator_Declaration_elaborate___lambda__1___boxed), 9, 5);
+x_136 = l_Lean_Elaborator_declaration_elaborate___closed__3;
+x_137 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elaborator_declaration_elaborate___lambda__1___boxed), 9, 5);
 lean::closure_set(x_137, 0, x_125);
 lean::closure_set(x_137, 1, x_128);
 lean::closure_set(x_137, 2, x_131);
 lean::closure_set(x_137, 3, x_136);
 lean::closure_set(x_137, 4, x_0);
-x_138 = lean::alloc_closure(reinterpret_cast<void*>(l_ReaderT_bind___at_Lean_Elaborator_Declaration_elaborate___spec__1___rarg), 5, 2);
+x_138 = lean::alloc_closure(reinterpret_cast<void*>(l_ReaderT_bind___at_Lean_Elaborator_declaration_elaborate___spec__1___rarg), 5, 2);
 lean::closure_set(x_138, 0, x_135);
 lean::closure_set(x_138, 1, x_137);
 x_139 = l_Lean_Elaborator_locally(x_138, x_1, x_2, x_3);
@@ -17111,8 +17088,8 @@ lean::dec(x_11);
 lean::inc(x_173);
 x_177 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elaborator_declModifiersToPexpr___boxed), 4, 1);
 lean::closure_set(x_177, 0, x_173);
-x_178 = l_Lean_Elaborator_Declaration_elaborate___closed__4;
-x_179 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elaborator_Declaration_elaborate___lambda__2___boxed), 13, 9);
+x_178 = l_Lean_Elaborator_declaration_elaborate___closed__4;
+x_179 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elaborator_declaration_elaborate___lambda__2___boxed), 13, 9);
 lean::closure_set(x_179, 0, x_172);
 lean::closure_set(x_179, 1, x_161);
 lean::closure_set(x_179, 2, x_166);
@@ -17122,7 +17099,7 @@ lean::closure_set(x_179, 5, x_163);
 lean::closure_set(x_179, 6, x_178);
 lean::closure_set(x_179, 7, x_159);
 lean::closure_set(x_179, 8, x_173);
-x_180 = lean::alloc_closure(reinterpret_cast<void*>(l_ReaderT_bind___at_Lean_Elaborator_Declaration_elaborate___spec__1___rarg), 5, 2);
+x_180 = lean::alloc_closure(reinterpret_cast<void*>(l_ReaderT_bind___at_Lean_Elaborator_declaration_elaborate___spec__1___rarg), 5, 2);
 lean::closure_set(x_180, 0, x_177);
 lean::closure_set(x_180, 1, x_179);
 x_181 = l_Lean_Elaborator_locally(x_180, x_1, x_2, x_3);
@@ -17193,8 +17170,8 @@ lean::inc(x_219);
 lean::dec(x_11);
 x_222 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elaborator_declModifiersToPexpr___boxed), 4, 1);
 lean::closure_set(x_222, 0, x_219);
-x_223 = l_Lean_Elaborator_Declaration_elaborate___closed__5;
-x_224 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elaborator_Declaration_elaborate___lambda__3___boxed), 14, 10);
+x_223 = l_Lean_Elaborator_declaration_elaborate___closed__5;
+x_224 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elaborator_declaration_elaborate___lambda__3___boxed), 14, 10);
 lean::closure_set(x_224, 0, x_203);
 lean::closure_set(x_224, 1, x_212);
 lean::closure_set(x_224, 2, x_215);
@@ -17205,7 +17182,7 @@ lean::closure_set(x_224, 6, x_218);
 lean::closure_set(x_224, 7, x_223);
 lean::closure_set(x_224, 8, x_205);
 lean::closure_set(x_224, 9, x_201);
-x_225 = lean::alloc_closure(reinterpret_cast<void*>(l_ReaderT_bind___at_Lean_Elaborator_Declaration_elaborate___spec__1___rarg), 5, 2);
+x_225 = lean::alloc_closure(reinterpret_cast<void*>(l_ReaderT_bind___at_Lean_Elaborator_declaration_elaborate___spec__1___rarg), 5, 2);
 lean::closure_set(x_225, 0, x_222);
 lean::closure_set(x_225, 1, x_224);
 x_226 = l_Lean_Elaborator_locally(x_225, x_1, x_2, x_3);
@@ -17230,7 +17207,7 @@ obj* x_232; obj* x_233; obj* x_234; obj* x_235;
 lean::dec(x_4);
 x_232 = lean::alloc_cnstr(1, 1, 0);
 lean::cnstr_set(x_232, 0, x_0);
-x_233 = l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2___closed__1;
+x_233 = l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2___closed__1;
 x_234 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Expander_error___at_Lean_Elaborator_currentScope___spec__1___rarg___boxed), 5, 2);
 lean::closure_set(x_234, 0, x_232);
 lean::closure_set(x_234, 1, x_233);
@@ -17239,69 +17216,69 @@ return x_235;
 }
 }
 }
-obj* l_ReaderT_bind___at_Lean_Elaborator_Declaration_elaborate___spec__1___boxed(obj* x_0, obj* x_1) {
+obj* l_ReaderT_bind___at_Lean_Elaborator_declaration_elaborate___spec__1___boxed(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; 
-x_2 = l_ReaderT_bind___at_Lean_Elaborator_Declaration_elaborate___spec__1(x_0, x_1);
+x_2 = l_ReaderT_bind___at_Lean_Elaborator_declaration_elaborate___spec__1(x_0, x_1);
 lean::dec(x_0);
 lean::dec(x_1);
 return x_2;
 }
 }
-obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+obj* l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
 obj* x_5; 
-x_5 = l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2(x_0, x_1, x_2, x_3, x_4);
+x_5 = l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2(x_0, x_1, x_2, x_3, x_4);
 lean::dec(x_2);
 return x_5;
 }
 }
-obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__4___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+obj* l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__4___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 obj* x_4; 
-x_4 = l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__4(x_0, x_1, x_2, x_3);
+x_4 = l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__4(x_0, x_1, x_2, x_3);
 lean::dec(x_1);
 return x_4;
 }
 }
-obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__5___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
+obj* l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__5___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
 _start:
 {
 obj* x_6; 
-x_6 = l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__5(x_0, x_1, x_2, x_3, x_4, x_5);
+x_6 = l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__5(x_0, x_1, x_2, x_3, x_4, x_5);
 lean::dec(x_3);
 return x_6;
 }
 }
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8) {
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8) {
 _start:
 {
 obj* x_9; 
-x_9 = l_Lean_Elaborator_Declaration_elaborate___lambda__1(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
+x_9 = l_Lean_Elaborator_declaration_elaborate___lambda__1(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
 lean::dec(x_4);
 lean::dec(x_6);
 return x_9;
 }
 }
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__2___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8, obj* x_9, obj* x_10, obj* x_11, obj* x_12) {
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__2___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8, obj* x_9, obj* x_10, obj* x_11, obj* x_12) {
 _start:
 {
 obj* x_13; 
-x_13 = l_Lean_Elaborator_Declaration_elaborate___lambda__2(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
+x_13 = l_Lean_Elaborator_declaration_elaborate___lambda__2(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
 lean::dec(x_2);
 lean::dec(x_8);
 lean::dec(x_10);
 return x_13;
 }
 }
-obj* l_Lean_Elaborator_Declaration_elaborate___lambda__3___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8, obj* x_9, obj* x_10, obj* x_11, obj* x_12, obj* x_13) {
+obj* l_Lean_Elaborator_declaration_elaborate___lambda__3___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8, obj* x_9, obj* x_10, obj* x_11, obj* x_12, obj* x_13) {
 _start:
 {
 obj* x_14; 
-x_14 = l_Lean_Elaborator_Declaration_elaborate___lambda__3(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
+x_14 = l_Lean_Elaborator_declaration_elaborate___lambda__3(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
 lean::dec(x_1);
 lean::dec(x_8);
 lean::dec(x_11);
@@ -17355,7 +17332,7 @@ lean::cnstr_set(x_28, 0, x_23);
 lean::cnstr_set(x_28, 1, x_25);
 lean::cnstr_set_scalar(x_28, sizeof(void*)*2, x_1);
 x_29 = x_28;
-x_30 = l_Lean_Elaborator_toLevel___main___closed__4;
+x_30 = l_Lean_SMap_insert___main___at_Lean_Environment_add___spec__1___closed__1;
 x_31 = l_Lean_Elaborator_OrderedRBMap_insert___rarg(x_30, x_12, x_2, x_29);
 if (lean::is_scalar(x_22)) {
  x_32 = lean::alloc_cnstr(0, 9, 0);
@@ -17488,7 +17465,7 @@ x_55 = l_Lean_Elaborator_mangleIdent(x_21);
 x_56 = lean::cnstr_get(x_50, 4);
 lean::inc(x_56);
 lean::dec(x_50);
-x_59 = l_Lean_Elaborator_toLevel___main___closed__4;
+x_59 = l_Lean_SMap_insert___main___at_Lean_Environment_add___spec__1___closed__1;
 lean::inc(x_55);
 x_61 = l_Lean_Elaborator_OrderedRBMap_find___rarg(x_59, x_56, x_55);
 if (lean::obj_tag(x_61) == 0)
@@ -21729,7 +21706,7 @@ if (lean::is_exclusive(x_1)) {
 }
 lean::inc(x_0);
 x_22 = level_mk_param(x_0);
-x_23 = l_Lean_Elaborator_toLevel___main___closed__4;
+x_23 = l_Lean_SMap_insert___main___at_Lean_Environment_add___spec__1___closed__1;
 x_24 = l_Lean_Elaborator_OrderedRBMap_insert___rarg(x_23, x_8, x_0, x_22);
 if (lean::is_scalar(x_20)) {
  x_25 = lean::alloc_cnstr(0, 9, 0);
@@ -21816,7 +21793,7 @@ lean::dec(x_23);
 x_31 = lean::cnstr_get(x_26, 3);
 lean::inc(x_31);
 lean::dec(x_26);
-x_34 = l_Lean_Elaborator_toLevel___main___closed__4;
+x_34 = l_Lean_SMap_insert___main___at_Lean_Environment_add___spec__1___closed__1;
 lean::inc(x_13);
 x_36 = l_Lean_Elaborator_OrderedRBMap_find___rarg(x_34, x_31, x_13);
 if (lean::obj_tag(x_36) == 0)
@@ -25172,8 +25149,8 @@ x_28 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elaborator_include_ela
 x_29 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_29, 0, x_27);
 lean::cnstr_set(x_29, 1, x_28);
-x_30 = l_Lean_Parser_command_Declaration;
-x_31 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elaborator_Declaration_elaborate), 4, 0);
+x_30 = l_Lean_Parser_command_declaration;
+x_31 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elaborator_declaration_elaborate), 4, 0);
 x_32 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_32, 0, x_30);
 lean::cnstr_set(x_32, 1, x_31);
@@ -25584,50 +25561,52 @@ _start:
 {
 if (lean::obj_tag(x_2) == 0)
 {
-obj* x_5; 
+obj* x_6; 
+lean::dec(x_1);
 lean::dec(x_0);
-x_5 = l_List_reverse___rarg(x_3);
-return x_5;
+x_6 = l_List_reverse___rarg(x_3);
+return x_6;
 }
 else
 {
-obj* x_6; obj* x_8; obj* x_10; obj* x_11; obj* x_13; uint8 x_14; 
-x_6 = lean::cnstr_get(x_2, 0);
-x_8 = lean::cnstr_get(x_2, 1);
+obj* x_7; obj* x_9; obj* x_11; obj* x_12; obj* x_15; uint8 x_16; 
+x_7 = lean::cnstr_get(x_2, 0);
+x_9 = lean::cnstr_get(x_2, 1);
 if (lean::is_exclusive(x_2)) {
  lean::cnstr_set(x_2, 0, lean::box(0));
  lean::cnstr_set(x_2, 1, lean::box(0));
- x_10 = x_2;
+ x_11 = x_2;
 } else {
- lean::inc(x_6);
- lean::inc(x_8);
+ lean::inc(x_7);
+ lean::inc(x_9);
  lean::dec(x_2);
- x_10 = lean::box(0);
+ x_11 = lean::box(0);
 }
-x_11 = lean::cnstr_get(x_1, 8);
+x_12 = lean::cnstr_get(x_1, 8);
+lean::inc(x_12);
 lean::inc(x_0);
-x_13 = l_Lean_Name_append___main(x_6, x_0);
-x_14 = lean_environment_contains(x_11, x_13);
-lean::dec(x_13);
-if (x_14 == 0)
+x_15 = l_Lean_Name_append___main(x_7, x_0);
+x_16 = l_Lean_Environment_contains(x_12, x_15);
+lean::dec(x_15);
+if (x_16 == 0)
 {
-lean::dec(x_6);
-lean::dec(x_10);
-x_2 = x_8;
+lean::dec(x_7);
+lean::dec(x_11);
+x_2 = x_9;
 goto _start;
 }
 else
 {
-obj* x_19; 
-if (lean::is_scalar(x_10)) {
- x_19 = lean::alloc_cnstr(1, 2, 0);
+obj* x_21; 
+if (lean::is_scalar(x_11)) {
+ x_21 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_19 = x_10;
+ x_21 = x_11;
 }
-lean::cnstr_set(x_19, 0, x_6);
-lean::cnstr_set(x_19, 1, x_3);
-x_2 = x_8;
-x_3 = x_19;
+lean::cnstr_set(x_21, 0, x_7);
+lean::cnstr_set(x_21, 1, x_3);
+x_2 = x_9;
+x_3 = x_21;
 goto _start;
 }
 }
@@ -25690,45 +25669,47 @@ _start:
 {
 if (lean::obj_tag(x_1) == 0)
 {
-obj* x_3; 
-x_3 = l_List_reverse___rarg(x_2);
-return x_3;
+obj* x_4; 
+lean::dec(x_0);
+x_4 = l_List_reverse___rarg(x_2);
+return x_4;
 }
 else
 {
-obj* x_4; obj* x_6; obj* x_8; uint8 x_9; 
-x_4 = lean::cnstr_get(x_1, 0);
-x_6 = lean::cnstr_get(x_1, 1);
+obj* x_5; obj* x_7; obj* x_9; uint8 x_11; 
+x_5 = lean::cnstr_get(x_1, 0);
+x_7 = lean::cnstr_get(x_1, 1);
 if (lean::is_exclusive(x_1)) {
  lean::cnstr_set(x_1, 0, lean::box(0));
  lean::cnstr_set(x_1, 1, lean::box(0));
- x_8 = x_1;
+ x_9 = x_1;
 } else {
- lean::inc(x_4);
- lean::inc(x_6);
+ lean::inc(x_5);
+ lean::inc(x_7);
  lean::dec(x_1);
- x_8 = lean::box(0);
+ x_9 = lean::box(0);
 }
-x_9 = lean_environment_contains(x_0, x_4);
-if (x_9 == 0)
+lean::inc(x_0);
+x_11 = l_Lean_Environment_contains(x_0, x_5);
+if (x_11 == 0)
 {
-lean::dec(x_4);
-lean::dec(x_8);
-x_1 = x_6;
+lean::dec(x_5);
+lean::dec(x_9);
+x_1 = x_7;
 goto _start;
 }
 else
 {
-obj* x_13; 
-if (lean::is_scalar(x_8)) {
- x_13 = lean::alloc_cnstr(1, 2, 0);
+obj* x_15; 
+if (lean::is_scalar(x_9)) {
+ x_15 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_13 = x_8;
+ x_15 = x_9;
 }
-lean::cnstr_set(x_13, 0, x_4);
-lean::cnstr_set(x_13, 1, x_2);
-x_1 = x_6;
-x_2 = x_13;
+lean::cnstr_set(x_15, 0, x_5);
+lean::cnstr_set(x_15, 1, x_2);
+x_1 = x_7;
+x_2 = x_15;
 goto _start;
 }
 }
@@ -25846,45 +25827,47 @@ _start:
 {
 if (lean::obj_tag(x_1) == 0)
 {
-obj* x_3; 
-x_3 = l_List_reverse___rarg(x_2);
-return x_3;
+obj* x_4; 
+lean::dec(x_0);
+x_4 = l_List_reverse___rarg(x_2);
+return x_4;
 }
 else
 {
-obj* x_4; obj* x_6; obj* x_8; uint8 x_9; 
-x_4 = lean::cnstr_get(x_1, 0);
-x_6 = lean::cnstr_get(x_1, 1);
+obj* x_5; obj* x_7; obj* x_9; uint8 x_11; 
+x_5 = lean::cnstr_get(x_1, 0);
+x_7 = lean::cnstr_get(x_1, 1);
 if (lean::is_exclusive(x_1)) {
  lean::cnstr_set(x_1, 0, lean::box(0));
  lean::cnstr_set(x_1, 1, lean::box(0));
- x_8 = x_1;
+ x_9 = x_1;
 } else {
- lean::inc(x_4);
- lean::inc(x_6);
+ lean::inc(x_5);
+ lean::inc(x_7);
  lean::dec(x_1);
- x_8 = lean::box(0);
+ x_9 = lean::box(0);
 }
-x_9 = lean_environment_contains(x_0, x_4);
-if (x_9 == 0)
+lean::inc(x_0);
+x_11 = l_Lean_Environment_contains(x_0, x_5);
+if (x_11 == 0)
 {
-lean::dec(x_4);
-lean::dec(x_8);
-x_1 = x_6;
+lean::dec(x_5);
+lean::dec(x_9);
+x_1 = x_7;
 goto _start;
 }
 else
 {
-obj* x_13; 
-if (lean::is_scalar(x_8)) {
- x_13 = lean::alloc_cnstr(1, 2, 0);
+obj* x_15; 
+if (lean::is_scalar(x_9)) {
+ x_15 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_13 = x_8;
+ x_15 = x_9;
 }
-lean::cnstr_set(x_13, 0, x_4);
-lean::cnstr_set(x_13, 1, x_2);
-x_1 = x_6;
-x_2 = x_13;
+lean::cnstr_set(x_15, 0, x_5);
+lean::cnstr_set(x_15, 1, x_2);
+x_1 = x_7;
+x_2 = x_15;
 goto _start;
 }
 }
@@ -25953,186 +25936,170 @@ if (lean::is_exclusive(x_12)) {
 }
 x_20 = lean::cnstr_get(x_15, 4);
 lean::inc(x_20);
-x_22 = l_Lean_Elaborator_toLevel___main___closed__4;
+x_22 = l_Lean_SMap_insert___main___at_Lean_Environment_add___spec__1___closed__1;
 lean::inc(x_0);
 x_24 = l_Lean_Elaborator_OrderedRBMap_find___rarg(x_22, x_20, x_0);
 if (lean::obj_tag(x_24) == 0)
 {
-obj* x_25; obj* x_27; obj* x_29; 
+obj* x_25; obj* x_27; obj* x_30; 
 x_25 = lean::cnstr_get(x_15, 6);
 lean::inc(x_25);
 x_27 = lean::box(0);
+lean::inc(x_3);
 lean::inc(x_0);
-x_29 = l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__1(x_0, x_3, x_25, x_27);
-if (lean::obj_tag(x_29) == 0)
+x_30 = l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__1(x_0, x_3, x_25, x_27);
+if (lean::obj_tag(x_30) == 0)
 {
-obj* x_30; obj* x_31; obj* x_33; obj* x_34; uint8 x_36; obj* x_37; obj* x_40; obj* x_41; obj* x_42; obj* x_45; obj* x_47; obj* x_48; 
-x_30 = l_Lean_Elaborator_resolveContext___main___closed__1;
-x_31 = lean::box(0);
+obj* x_31; obj* x_32; obj* x_34; obj* x_35; uint8 x_38; obj* x_39; obj* x_42; obj* x_44; obj* x_45; obj* x_48; obj* x_50; obj* x_51; 
+x_31 = l_Lean_Elaborator_resolveContext___main___closed__1;
+x_32 = lean::box(0);
 lean::inc(x_0);
-x_33 = l_Lean_Name_replacePrefix___main(x_0, x_30, x_31);
-x_34 = lean::cnstr_get(x_3, 8);
-lean::inc(x_34);
-x_36 = lean_environment_contains(x_34, x_33);
-x_37 = lean::cnstr_get(x_15, 7);
-lean::inc(x_37);
+x_34 = l_Lean_Name_replacePrefix___main(x_0, x_31, x_32);
+x_35 = lean::cnstr_get(x_3, 8);
+lean::inc(x_35);
+lean::inc(x_35);
+x_38 = l_Lean_Environment_contains(x_35, x_34);
+x_39 = lean::cnstr_get(x_15, 7);
+lean::inc(x_39);
 lean::inc(x_0);
-x_40 = l_List_filterMap___main___at_Lean_Elaborator_resolveContext___main___spec__2(x_0, x_37);
-x_41 = l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__3(x_34, x_40, x_27);
-x_42 = lean::cnstr_get(x_3, 3);
-lean::inc(x_42);
+x_42 = l_List_filterMap___main___at_Lean_Elaborator_resolveContext___main___spec__2(x_0, x_39);
+lean::inc(x_35);
+x_44 = l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__3(x_35, x_42, x_27);
+x_45 = lean::cnstr_get(x_3, 3);
+lean::inc(x_45);
 lean::dec(x_3);
-x_45 = l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__4(x_15, x_42, x_27);
+x_48 = l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__4(x_15, x_45, x_27);
 lean::dec(x_15);
-x_47 = l_List_filterMap___main___at_Lean_Elaborator_resolveContext___main___spec__5(x_0, x_45);
-x_48 = l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__6(x_34, x_47, x_27);
+x_50 = l_List_filterMap___main___at_Lean_Elaborator_resolveContext___main___spec__5(x_0, x_48);
+x_51 = l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__6(x_35, x_50, x_27);
+if (x_38 == 0)
+{
+obj* x_53; obj* x_54; obj* x_55; obj* x_56; 
 lean::dec(x_34);
-if (x_36 == 0)
-{
-obj* x_51; obj* x_52; obj* x_53; obj* x_54; 
-lean::dec(x_33);
-x_51 = l_List_append___rarg(x_29, x_41);
-x_52 = l_List_append___rarg(x_51, x_48);
+x_53 = l_List_append___rarg(x_30, x_44);
+x_54 = l_List_append___rarg(x_53, x_51);
 if (lean::is_scalar(x_19)) {
- x_53 = lean::alloc_cnstr(0, 2, 0);
+ x_55 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_53 = x_19;
+ x_55 = x_19;
 }
-lean::cnstr_set(x_53, 0, x_52);
-lean::cnstr_set(x_53, 1, x_17);
+lean::cnstr_set(x_55, 0, x_54);
+lean::cnstr_set(x_55, 1, x_17);
 if (lean::is_scalar(x_14)) {
- x_54 = lean::alloc_cnstr(1, 1, 0);
+ x_56 = lean::alloc_cnstr(1, 1, 0);
 } else {
- x_54 = x_14;
+ x_56 = x_14;
 }
-lean::cnstr_set(x_54, 0, x_53);
-return x_54;
+lean::cnstr_set(x_56, 0, x_55);
+return x_56;
 }
 else
 {
-obj* x_55; obj* x_56; obj* x_57; obj* x_58; obj* x_59; 
-x_55 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_55, 0, x_33);
-lean::cnstr_set(x_55, 1, x_29);
-x_56 = l_List_append___rarg(x_55, x_41);
-x_57 = l_List_append___rarg(x_56, x_48);
+obj* x_57; obj* x_58; obj* x_59; obj* x_60; obj* x_61; 
+x_57 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_57, 0, x_34);
+lean::cnstr_set(x_57, 1, x_30);
+x_58 = l_List_append___rarg(x_57, x_44);
+x_59 = l_List_append___rarg(x_58, x_51);
 if (lean::is_scalar(x_19)) {
- x_58 = lean::alloc_cnstr(0, 2, 0);
+ x_60 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_58 = x_19;
+ x_60 = x_19;
 }
-lean::cnstr_set(x_58, 0, x_57);
-lean::cnstr_set(x_58, 1, x_17);
+lean::cnstr_set(x_60, 0, x_59);
+lean::cnstr_set(x_60, 1, x_17);
 if (lean::is_scalar(x_14)) {
- x_59 = lean::alloc_cnstr(1, 1, 0);
+ x_61 = lean::alloc_cnstr(1, 1, 0);
 } else {
- x_59 = x_14;
+ x_61 = x_14;
 }
-lean::cnstr_set(x_59, 0, x_58);
-return x_59;
+lean::cnstr_set(x_61, 0, x_60);
+return x_61;
 }
 }
 else
 {
-obj* x_62; obj* x_64; obj* x_65; obj* x_67; obj* x_68; obj* x_69; 
+obj* x_64; obj* x_66; obj* x_67; obj* x_69; obj* x_70; obj* x_71; 
 lean::dec(x_3);
 lean::dec(x_15);
-x_62 = lean::cnstr_get(x_29, 0);
-if (lean::is_exclusive(x_29)) {
- lean::cnstr_release(x_29, 1);
- x_64 = x_29;
+x_64 = lean::cnstr_get(x_30, 0);
+if (lean::is_exclusive(x_30)) {
+ lean::cnstr_release(x_30, 1);
+ x_66 = x_30;
 } else {
- lean::inc(x_62);
- lean::dec(x_29);
- x_64 = lean::box(0);
+ lean::inc(x_64);
+ lean::dec(x_30);
+ x_66 = lean::box(0);
 }
-x_65 = l_Lean_Name_append___main(x_62, x_0);
-lean::dec(x_62);
-if (lean::is_scalar(x_64)) {
- x_67 = lean::alloc_cnstr(1, 2, 0);
+x_67 = l_Lean_Name_append___main(x_64, x_0);
+lean::dec(x_64);
+if (lean::is_scalar(x_66)) {
+ x_69 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_67 = x_64;
+ x_69 = x_66;
 }
-lean::cnstr_set(x_67, 0, x_65);
-lean::cnstr_set(x_67, 1, x_27);
+lean::cnstr_set(x_69, 0, x_67);
+lean::cnstr_set(x_69, 1, x_27);
 if (lean::is_scalar(x_19)) {
- x_68 = lean::alloc_cnstr(0, 2, 0);
+ x_70 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_68 = x_19;
+ x_70 = x_19;
 }
-lean::cnstr_set(x_68, 0, x_67);
-lean::cnstr_set(x_68, 1, x_17);
+lean::cnstr_set(x_70, 0, x_69);
+lean::cnstr_set(x_70, 1, x_17);
 if (lean::is_scalar(x_14)) {
- x_69 = lean::alloc_cnstr(1, 1, 0);
+ x_71 = lean::alloc_cnstr(1, 1, 0);
 } else {
- x_69 = x_14;
+ x_71 = x_14;
 }
-lean::cnstr_set(x_69, 0, x_68);
-return x_69;
+lean::cnstr_set(x_71, 0, x_70);
+return x_71;
 }
 }
 else
 {
-obj* x_74; obj* x_77; obj* x_79; obj* x_80; obj* x_83; obj* x_84; obj* x_85; obj* x_86; 
+obj* x_76; obj* x_79; obj* x_81; obj* x_82; obj* x_85; obj* x_86; obj* x_87; obj* x_88; 
 lean::dec(x_3);
 lean::dec(x_0);
 lean::dec(x_15);
 lean::dec(x_19);
-x_74 = lean::cnstr_get(x_24, 0);
-lean::inc(x_74);
+x_76 = lean::cnstr_get(x_24, 0);
+lean::inc(x_76);
 lean::dec(x_24);
-x_77 = lean::cnstr_get(x_74, 1);
-if (lean::is_exclusive(x_74)) {
- lean::cnstr_release(x_74, 0);
- x_79 = x_74;
+x_79 = lean::cnstr_get(x_76, 1);
+if (lean::is_exclusive(x_76)) {
+ lean::cnstr_release(x_76, 0);
+ x_81 = x_76;
 } else {
- lean::inc(x_77);
- lean::dec(x_74);
- x_79 = lean::box(0);
+ lean::inc(x_79);
+ lean::dec(x_76);
+ x_81 = lean::box(0);
 }
-x_80 = lean::cnstr_get(x_77, 0);
-lean::inc(x_80);
-lean::dec(x_77);
-x_83 = lean::box(0);
-x_84 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_84, 0, x_80);
-lean::cnstr_set(x_84, 1, x_83);
-if (lean::is_scalar(x_79)) {
- x_85 = lean::alloc_cnstr(0, 2, 0);
+x_82 = lean::cnstr_get(x_79, 0);
+lean::inc(x_82);
+lean::dec(x_79);
+x_85 = lean::box(0);
+x_86 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_86, 0, x_82);
+lean::cnstr_set(x_86, 1, x_85);
+if (lean::is_scalar(x_81)) {
+ x_87 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_85 = x_79;
+ x_87 = x_81;
 }
-lean::cnstr_set(x_85, 0, x_84);
-lean::cnstr_set(x_85, 1, x_17);
+lean::cnstr_set(x_87, 0, x_86);
+lean::cnstr_set(x_87, 1, x_17);
 if (lean::is_scalar(x_14)) {
- x_86 = lean::alloc_cnstr(1, 1, 0);
+ x_88 = lean::alloc_cnstr(1, 1, 0);
 } else {
- x_86 = x_14;
+ x_88 = x_14;
 }
-lean::cnstr_set(x_86, 0, x_85);
-return x_86;
+lean::cnstr_set(x_88, 0, x_87);
+return x_88;
 }
 }
 }
 }
-obj* l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__1(x_0, x_1, x_2, x_3);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__3___boxed(obj* x_0, obj* x_1, obj* x_2) {
-_start:
-{
-obj* x_3; 
-x_3 = l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__3(x_0, x_1, x_2);
-lean::dec(x_0);
-return x_3;
-}
-}
 obj* l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__4___boxed(obj* x_0, obj* x_1, obj* x_2) {
 _start:
 {
@@ -26142,15 +26109,6 @@ lean::dec(x_0);
 return x_3;
 }
 }
-obj* l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__6___boxed(obj* x_0, obj* x_1, obj* x_2) {
-_start:
-{
-obj* x_3; 
-x_3 = l_List_filterAux___main___at_Lean_Elaborator_resolveContext___main___spec__6(x_0, x_1, x_2);
-lean::dec(x_0);
-return x_3;
-}
-}
 obj* l_Lean_Elaborator_resolveContext___main___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
@@ -27189,6 +27147,7 @@ obj* initialize_init_lean_parser_module(obj*);
 obj* initialize_init_lean_expander(obj*);
 obj* initialize_init_lean_expr(obj*);
 obj* initialize_init_lean_options(obj*);
+obj* initialize_init_lean_environment(obj*);
 static bool _G_initialized = false;
 obj* initialize_init_lean_elaborator(obj* w) {
  if (_G_initialized) return w;
@@ -27201,6 +27160,8 @@ if (io_result_is_error(w)) return w;
 w = initialize_init_lean_expr(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_options(w);
+if (io_result_is_error(w)) return w;
+w = initialize_init_lean_environment(w);
 if (io_result_is_error(w)) return w;
  l_Lean_Elaborator_ElaboratorM_Monad = _init_l_Lean_Elaborator_ElaboratorM_Monad();
 lean::mark_persistent(l_Lean_Elaborator_ElaboratorM_Monad);
@@ -27228,8 +27189,6 @@ lean::mark_persistent(l_Lean_Elaborator_toLevel___main___closed__2);
 lean::mark_persistent(l_Lean_Elaborator_toLevel___main___closed__3);
  l_Lean_Elaborator_toLevel___main___closed__4 = _init_l_Lean_Elaborator_toLevel___main___closed__4();
 lean::mark_persistent(l_Lean_Elaborator_toLevel___main___closed__4);
- l_Lean_Elaborator_toLevel___main___closed__5 = _init_l_Lean_Elaborator_toLevel___main___closed__5();
-lean::mark_persistent(l_Lean_Elaborator_toLevel___main___closed__5);
  l_Lean_Elaborator_Expr_mkAnnotation___closed__1 = _init_l_Lean_Elaborator_Expr_mkAnnotation___closed__1();
 lean::mark_persistent(l_Lean_Elaborator_Expr_mkAnnotation___closed__1);
  l_Lean_Elaborator_dummy = _init_l_Lean_Elaborator_dummy();
@@ -27362,22 +27321,22 @@ lean::mark_persistent(l_Lean_Elaborator_inferModToPexpr___closed__1);
 lean::mark_persistent(l_Lean_Elaborator_inferModToPexpr___closed__2);
  l_Lean_Elaborator_inferModToPexpr___closed__3 = _init_l_Lean_Elaborator_inferModToPexpr___closed__3();
 lean::mark_persistent(l_Lean_Elaborator_inferModToPexpr___closed__3);
- l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2___closed__1 = _init_l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2___closed__1();
-lean::mark_persistent(l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__2___closed__1);
- l_Lean_Elaborator_Declaration_elaborate___lambda__3___closed__1 = _init_l_Lean_Elaborator_Declaration_elaborate___lambda__3___closed__1();
-lean::mark_persistent(l_Lean_Elaborator_Declaration_elaborate___lambda__3___closed__1);
- l_Lean_Elaborator_Declaration_elaborate___lambda__3___closed__2 = _init_l_Lean_Elaborator_Declaration_elaborate___lambda__3___closed__2();
-lean::mark_persistent(l_Lean_Elaborator_Declaration_elaborate___lambda__3___closed__2);
- l_Lean_Elaborator_Declaration_elaborate___closed__1 = _init_l_Lean_Elaborator_Declaration_elaborate___closed__1();
-lean::mark_persistent(l_Lean_Elaborator_Declaration_elaborate___closed__1);
- l_Lean_Elaborator_Declaration_elaborate___closed__2 = _init_l_Lean_Elaborator_Declaration_elaborate___closed__2();
-lean::mark_persistent(l_Lean_Elaborator_Declaration_elaborate___closed__2);
- l_Lean_Elaborator_Declaration_elaborate___closed__3 = _init_l_Lean_Elaborator_Declaration_elaborate___closed__3();
-lean::mark_persistent(l_Lean_Elaborator_Declaration_elaborate___closed__3);
- l_Lean_Elaborator_Declaration_elaborate___closed__4 = _init_l_Lean_Elaborator_Declaration_elaborate___closed__4();
-lean::mark_persistent(l_Lean_Elaborator_Declaration_elaborate___closed__4);
- l_Lean_Elaborator_Declaration_elaborate___closed__5 = _init_l_Lean_Elaborator_Declaration_elaborate___closed__5();
-lean::mark_persistent(l_Lean_Elaborator_Declaration_elaborate___closed__5);
+ l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2___closed__1 = _init_l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2___closed__1();
+lean::mark_persistent(l_List_mmap___main___at_Lean_Elaborator_declaration_elaborate___spec__2___closed__1);
+ l_Lean_Elaborator_declaration_elaborate___lambda__3___closed__1 = _init_l_Lean_Elaborator_declaration_elaborate___lambda__3___closed__1();
+lean::mark_persistent(l_Lean_Elaborator_declaration_elaborate___lambda__3___closed__1);
+ l_Lean_Elaborator_declaration_elaborate___lambda__3___closed__2 = _init_l_Lean_Elaborator_declaration_elaborate___lambda__3___closed__2();
+lean::mark_persistent(l_Lean_Elaborator_declaration_elaborate___lambda__3___closed__2);
+ l_Lean_Elaborator_declaration_elaborate___closed__1 = _init_l_Lean_Elaborator_declaration_elaborate___closed__1();
+lean::mark_persistent(l_Lean_Elaborator_declaration_elaborate___closed__1);
+ l_Lean_Elaborator_declaration_elaborate___closed__2 = _init_l_Lean_Elaborator_declaration_elaborate___closed__2();
+lean::mark_persistent(l_Lean_Elaborator_declaration_elaborate___closed__2);
+ l_Lean_Elaborator_declaration_elaborate___closed__3 = _init_l_Lean_Elaborator_declaration_elaborate___closed__3();
+lean::mark_persistent(l_Lean_Elaborator_declaration_elaborate___closed__3);
+ l_Lean_Elaborator_declaration_elaborate___closed__4 = _init_l_Lean_Elaborator_declaration_elaborate___closed__4();
+lean::mark_persistent(l_Lean_Elaborator_declaration_elaborate___closed__4);
+ l_Lean_Elaborator_declaration_elaborate___closed__5 = _init_l_Lean_Elaborator_declaration_elaborate___closed__5();
+lean::mark_persistent(l_Lean_Elaborator_declaration_elaborate___closed__5);
  l_Lean_Elaborator_variables_elaborate___closed__1 = _init_l_Lean_Elaborator_variables_elaborate___closed__1();
 lean::mark_persistent(l_Lean_Elaborator_variables_elaborate___closed__1);
  l_Lean_Elaborator_variables_elaborate___closed__2 = _init_l_Lean_Elaborator_variables_elaborate___closed__2();
diff --git a/src/stage0/init/lean/environment.cpp b/src/stage0/init/lean/environment.cpp
index 513ce0bd91..82cc98a027 100644
--- a/src/stage0/init/lean/environment.cpp
+++ b/src/stage0/init/lean/environment.cpp
@@ -138,6 +138,7 @@ uint8 environment_quot_init_core(obj*);
 obj* l_Lean_SMap_switch___at___private_init_lean_environment_1__switch___spec__1(obj*);
 extern obj* l_NonScalar_Inhabited;
 obj* l_List_foldl___main___rarg(obj*, obj*, obj*);
+obj* l_Lean_Environment_contains___boxed(obj*, obj*);
 obj* l___private_init_lean_environment_3__isQuotInit___boxed(obj*);
 obj* l_Lean_PersistentEnvExtension_addEntry___boxed(obj*, obj*);
 obj* l_Lean_PersistentEnvExtension_getState___boxed(obj*, obj*);
@@ -189,6 +190,7 @@ extern obj* l_Lean_Name_toString___closed__1;
 namespace lean {
 uint8 nat_dec_le(obj*, obj*);
 }
+uint8 l_Lean_Environment_contains(obj*, obj*);
 namespace lean {
 uint32 environment_trust_level_core(obj*);
 }
@@ -1939,6 +1941,39 @@ lean::dec(x_1);
 return x_2;
 }
 }
+uint8 l_Lean_Environment_contains(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_5; 
+x_2 = lean::cnstr_get(x_0, 1);
+lean::inc(x_2);
+lean::dec(x_0);
+x_5 = l_Lean_SMap_find___main___at_Lean_Environment_find___spec__1(x_2, x_1);
+if (lean::obj_tag(x_5) == 0)
+{
+uint8 x_6; 
+x_6 = 0;
+return x_6;
+}
+else
+{
+uint8 x_8; 
+lean::dec(x_5);
+x_8 = 1;
+return x_8;
+}
+}
+}
+obj* l_Lean_Environment_contains___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+uint8 x_2; obj* x_3; 
+x_2 = l_Lean_Environment_contains(x_0, x_1);
+x_3 = lean::box(x_2);
+lean::dec(x_1);
+return x_3;
+}
+}
 obj* l_Lean_SMap_switch___at___private_init_lean_environment_1__switch___spec__1(obj* x_0) {
 _start:
 {
diff --git a/src/stage0/init/lean/expander.cpp b/src/stage0/init/lean/expander.cpp
index ef445f2b49..9f695f32c6 100644
--- a/src/stage0/init/lean/expander.cpp
+++ b/src/stage0/init/lean/expander.cpp
@@ -33,7 +33,6 @@ obj* l_Lean_Parser_Syntax_flipScopes___main(obj*, obj*);
 obj* l_Lean_Expander_mixfixToNotationSpec___closed__5;
 obj* l_Lean_Expander_coeBinderBracketedBinder___closed__1;
 obj* l_Lean_Expander_expandBracketedBinder___main(obj*, obj*);
-obj* l_Lean_Expander_Declaration_transform___boxed(obj*, obj*);
 obj* l_DList_singleton___elambda__1___rarg(obj*, obj*);
 obj* l_Lean_Parser_Syntax_mreplace___main___at_Lean_Parser_Syntax_replace___spec__1(obj*, obj*);
 extern obj* l_Lean_Parser_Term_hole_HasView;
@@ -63,7 +62,6 @@ obj* l_Lean_Expander_assume_transform___boxed(obj*, obj*);
 extern obj* l_Lean_Parser_command_mixfix;
 obj* l_Lean_Expander_paren_transform(obj*, obj*);
 obj* l_Lean_Expander_mkNotationTransformer___lambda__1(obj*, obj*);
-obj* l_Lean_Expander_Declaration_transform___closed__1;
 extern obj* l_Lean_Parser_command_reserveMixfix_HasView;
 obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__17(uint8, obj*, obj*);
 obj* l_Lean_Expander_let_transform___boxed(obj*, obj*);
@@ -115,6 +113,7 @@ obj* l_Lean_Expander_coeSimpleBinderBinders(obj*);
 extern obj* l_Lean_Parser_command_axiom_HasView;
 obj* l_Lean_Expander_paren_transform___closed__1;
 obj* l_Lean_Expander_TransformM_MonadReader;
+extern obj* l_Lean_Parser_command_declaration_HasView;
 extern obj* l_Lean_Parser_command_variables_HasView;
 obj* l_List_mfor___main___at_Lean_Expander_mkNotationTransformer___spec__4___closed__1;
 obj* l_Lean_Expander_mixfixToNotationSpec___closed__6;
@@ -166,6 +165,7 @@ obj* l_Lean_Expander_bindingAnnotationUpdate_Parser(obj*, obj*, obj*, obj*, obj*
 obj* l_Lean_Expander_introRule_transform(obj*, obj*);
 obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__18(uint8, obj*, obj*);
 extern obj* l_Lean_Parser_Term_depArrow_HasView;
+obj* l_Lean_Expander_declaration_transform(obj*, obj*);
 obj* l_RBNode_insert___at_Lean_Expander_builtinTransformers___spec__1(obj*, obj*, obj*);
 obj* l_Lean_Expander_Subtype_transform(obj*, obj*);
 obj* l_Lean_Parser_Syntax_getPos(obj*);
@@ -203,6 +203,8 @@ extern obj* l_Lean_Parser_Term_Subtype;
 obj* l_Lean_Expander_binderIdentToIdent___main___boxed(obj*);
 uint8 l_RBNode_isRed___main___rarg(obj*);
 obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__3(uint8, obj*, obj*);
+obj* l_Lean_Expander_declaration_transform___boxed(obj*, obj*);
+obj* l_Lean_Expander_declaration_transform___closed__3;
 obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__1___boxed(obj*, obj*, obj*);
 obj* l_Lean_Expander_mkSimpleBinder___closed__6;
 obj* l_List_mmap___main___at___private_init_lean_expander_2__expandCore___main___spec__5(obj*, obj*, obj*, obj*);
@@ -210,7 +212,6 @@ obj* l_Lean_Expander_error___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, ob
 extern obj* l_Lean_Parser_identUnivs;
 obj* l_List_lookup___main___at_Lean_Expander_mkNotationTransformer___spec__7___boxed(obj*, obj*);
 obj* l_Lean_Expander_ExpanderConfig_HasLift___boxed(obj*);
-extern obj* l_Lean_Parser_command_Declaration;
 extern obj* l_Lean_Parser_Term_Subtype_HasView;
 obj* l_Lean_Expander_ExpanderConfig_HasLift(obj*);
 obj* l_Lean_Expander_globId(obj*);
@@ -250,6 +251,7 @@ obj* l_Lean_Expander_coeBindersExtBinders(obj*);
 obj* l_List_map___main___at_Lean_Expander_coeMixedBindersBindersExt___spec__2___boxed(obj*);
 obj* l_Lean_Expander_universes_transform(obj*, obj*);
 obj* l_Lean_Expander_getOptType___main___boxed(obj*);
+extern obj* l_Lean_Parser_command_declaration;
 obj* l_Lean_Expander_coeBinderBracketedBinder___closed__2;
 obj* l_Lean_Expander_getOptType(obj*);
 extern obj* l_Lean_Parser_TermParserM_Monad;
@@ -266,9 +268,9 @@ obj* l_List_map___main___at_Lean_Expander_coeMixedBindersBindersExt___spec__2___
 extern obj* l_Lean_Parser_Term_anonymousConstructor_HasView;
 obj* l_Lean_Expander_TransformM_MonadExcept;
 obj* l_Lean_Expander_let_transform___closed__1;
-obj* l_Lean_Expander_Declaration_transform___closed__2;
 obj* l_Lean_Expander_mkSimpleBinder___closed__3;
 obj* l_Lean_Expander_introRule_transform___boxed(obj*, obj*);
+obj* l_Lean_Expander_declaration_transform___closed__2;
 obj* l_Lean_Expander_error___at___private_init_lean_expander_1__popStxArg___spec__1(obj*);
 obj* l_Lean_Parser_number_View_ofNat(obj*);
 obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__1(uint8, obj*, obj*);
@@ -280,6 +282,7 @@ obj* l_Lean_Expander_Subtype_transform___boxed(obj*, obj*);
 obj* l_List_foldr___main___at_Lean_Expander_expandBinders___spec__3___boxed(obj*, obj*, obj*);
 obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__11(obj*, obj*);
 obj* l_List_map___main___at___private_init_lean_expander_2__expandCore___main___spec__4(obj*, obj*);
+obj* l_Lean_Expander_declaration_transform___closed__1;
 extern obj* l_Lean_Parser_Term_arrow_HasView;
 obj* l_Lean_Expander_mkSimpleBinder___closed__7;
 obj* l_ExceptT_Monad___rarg(obj*);
@@ -298,9 +301,7 @@ obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__1
 obj* l_Lean_Expander_variable_transform___boxed(obj*, obj*);
 obj* l_Lean_Expander_axiom_transform___boxed(obj*, obj*);
 obj* l_Lean_Expander_coeIdentsBindersExt___boxed(obj*);
-obj* l_Lean_Expander_Declaration_transform(obj*, obj*);
 obj* l_Lean_Expander_coeMixedBindersBindersExt___rarg(obj*, obj*);
-obj* l_Lean_Expander_Declaration_transform___closed__3;
 obj* l_Lean_Expander_mixfix_transform(obj*, obj*);
 extern obj* l_Lean_Parser_Term_pi;
 obj* l_List_mmap___main___at_Lean_Expander_variables_transform___spec__1(obj*, obj*);
@@ -324,7 +325,6 @@ extern obj* l_Lean_Parser_Term_match_HasView;
 obj* l_RBNode_find___main___at___private_init_lean_expander_2__expandCore___main___spec__2(obj*, obj*);
 obj* l_Lean_Expander_mixfixToNotationSpec(obj*, obj*, obj*);
 obj* l_Lean_Parser_Substring_ofString(obj*);
-extern obj* l_Lean_Parser_command_Declaration_HasView;
 obj* l_Lean_Expander_mkSimpleBinder___closed__4;
 obj* l_Lean_Expander_noExpansion___closed__1;
 obj* l_Lean_Expander_binderIdentToIdent___main(obj*);
@@ -4872,7 +4872,7 @@ obj* _init_l_Lean_Expander_mixfixToNotationSpec___closed__7() {
 _start:
 {
 obj* x_0; 
-x_0 = lean::mk_string("invalid `infixr` Declaration, given precedence must greater than zero");
+x_0 = lean::mk_string("invalid `infixr` declaration, given precedence must greater than zero");
 return x_0;
 }
 }
@@ -9980,7 +9980,7 @@ lean::dec(x_1);
 return x_2;
 }
 }
-obj* _init_l_Lean_Expander_Declaration_transform___closed__1() {
+obj* _init_l_Lean_Expander_declaration_transform___closed__1() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_6; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; 
@@ -10034,7 +10034,7 @@ lean::cnstr_set(x_25, 0, x_24);
 return x_25;
 }
 }
-obj* _init_l_Lean_Expander_Declaration_transform___closed__2() {
+obj* _init_l_Lean_Expander_declaration_transform___closed__2() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_6; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; 
@@ -10063,7 +10063,7 @@ lean::cnstr_set(x_12, 1, x_3);
 return x_12;
 }
 }
-obj* _init_l_Lean_Expander_Declaration_transform___closed__3() {
+obj* _init_l_Lean_Expander_declaration_transform___closed__3() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; obj* x_4; obj* x_5; obj* x_6; 
@@ -10081,11 +10081,11 @@ lean::cnstr_set(x_6, 0, x_5);
 return x_6;
 }
 }
-obj* l_Lean_Expander_Declaration_transform(obj* x_0, obj* x_1) {
+obj* l_Lean_Expander_declaration_transform(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; obj* x_3; obj* x_5; obj* x_6; 
-x_2 = l_Lean_Parser_command_Declaration_HasView;
+x_2 = l_Lean_Parser_command_declaration_HasView;
 x_3 = lean::cnstr_get(x_2, 0);
 lean::inc(x_3);
 x_5 = lean::apply_1(x_3, x_0);
@@ -10193,7 +10193,7 @@ lean::cnstr_set(x_50, 0, x_49);
 if (lean::obj_tag(x_36) == 0)
 {
 obj* x_51; obj* x_52; obj* x_53; obj* x_54; obj* x_55; obj* x_56; 
-x_51 = l_Lean_Expander_Declaration_transform___closed__1;
+x_51 = l_Lean_Expander_declaration_transform___closed__1;
 if (lean::is_scalar(x_44)) {
  x_52 = lean::alloc_cnstr(0, 5, 0);
 } else {
@@ -10241,7 +10241,7 @@ if (lean::is_exclusive(x_57)) {
  lean::dec(x_57);
  x_66 = lean::box(0);
 }
-x_67 = l_Lean_Expander_Declaration_transform___closed__2;
+x_67 = l_Lean_Expander_declaration_transform___closed__2;
 x_68 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_68, 0, x_67);
 lean::cnstr_set(x_68, 1, x_62);
@@ -10361,7 +10361,7 @@ if (lean::is_exclusive(x_87)) {
 x_116 = lean::cnstr_get(x_2, 1);
 lean::inc(x_116);
 lean::dec(x_2);
-x_119 = l_Lean_Expander_Declaration_transform___closed__3;
+x_119 = l_Lean_Expander_declaration_transform___closed__3;
 if (lean::is_scalar(x_104)) {
  x_120 = lean::alloc_cnstr(0, 8, 0);
 } else {
@@ -10384,7 +10384,7 @@ lean::cnstr_set(x_121, 0, x_120);
 if (lean::obj_tag(x_107) == 0)
 {
 obj* x_122; obj* x_123; obj* x_124; obj* x_125; obj* x_126; obj* x_127; 
-x_122 = l_Lean_Expander_Declaration_transform___closed__1;
+x_122 = l_Lean_Expander_declaration_transform___closed__1;
 if (lean::is_scalar(x_115)) {
  x_123 = lean::alloc_cnstr(0, 5, 0);
 } else {
@@ -10428,7 +10428,7 @@ if (lean::is_exclusive(x_128)) {
  lean::dec(x_128);
  x_137 = lean::box(0);
 }
-x_138 = l_Lean_Expander_Declaration_transform___closed__2;
+x_138 = l_Lean_Expander_declaration_transform___closed__2;
 x_139 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_139, 0, x_138);
 lean::cnstr_set(x_139, 1, x_133);
@@ -10479,11 +10479,11 @@ return x_149;
 }
 }
 }
-obj* l_Lean_Expander_Declaration_transform___boxed(obj* x_0, obj* x_1) {
+obj* l_Lean_Expander_declaration_transform___boxed(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; 
-x_2 = l_Lean_Expander_Declaration_transform(x_0, x_1);
+x_2 = l_Lean_Expander_declaration_transform(x_0, x_1);
 lean::dec(x_1);
 return x_2;
 }
@@ -12757,8 +12757,8 @@ x_34 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Expander_axiom_transfo
 x_35 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_35, 0, x_33);
 lean::cnstr_set(x_35, 1, x_34);
-x_36 = l_Lean_Parser_command_Declaration;
-x_37 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Expander_Declaration_transform___boxed), 2, 0);
+x_36 = l_Lean_Parser_command_declaration;
+x_37 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Expander_declaration_transform___boxed), 2, 0);
 x_38 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_38, 0, x_36);
 lean::cnstr_set(x_38, 1, x_37);
@@ -13871,12 +13871,12 @@ lean::mark_persistent(l_Lean_Expander_if_transform___closed__3);
 lean::mark_persistent(l_Lean_Expander_let_transform___closed__1);
  l_Lean_Expander_axiom_transform___closed__1 = _init_l_Lean_Expander_axiom_transform___closed__1();
 lean::mark_persistent(l_Lean_Expander_axiom_transform___closed__1);
- l_Lean_Expander_Declaration_transform___closed__1 = _init_l_Lean_Expander_Declaration_transform___closed__1();
-lean::mark_persistent(l_Lean_Expander_Declaration_transform___closed__1);
- l_Lean_Expander_Declaration_transform___closed__2 = _init_l_Lean_Expander_Declaration_transform___closed__2();
-lean::mark_persistent(l_Lean_Expander_Declaration_transform___closed__2);
- l_Lean_Expander_Declaration_transform___closed__3 = _init_l_Lean_Expander_Declaration_transform___closed__3();
-lean::mark_persistent(l_Lean_Expander_Declaration_transform___closed__3);
+ l_Lean_Expander_declaration_transform___closed__1 = _init_l_Lean_Expander_declaration_transform___closed__1();
+lean::mark_persistent(l_Lean_Expander_declaration_transform___closed__1);
+ l_Lean_Expander_declaration_transform___closed__2 = _init_l_Lean_Expander_declaration_transform___closed__2();
+lean::mark_persistent(l_Lean_Expander_declaration_transform___closed__2);
+ l_Lean_Expander_declaration_transform___closed__3 = _init_l_Lean_Expander_declaration_transform___closed__3();
+lean::mark_persistent(l_Lean_Expander_declaration_transform___closed__3);
  l_Lean_Expander_variable_transform___closed__1 = _init_l_Lean_Expander_variable_transform___closed__1();
 lean::mark_persistent(l_Lean_Expander_variable_transform___closed__1);
  l_Lean_Expander_bindingAnnotationUpdate = _init_l_Lean_Expander_bindingAnnotationUpdate();
diff --git a/src/stage0/init/lean/parser/command.cpp b/src/stage0/init/lean/parser/command.cpp
index 4fdb0cf1fb..6a5cc64f6c 100644
--- a/src/stage0/init/lean/parser/command.cpp
+++ b/src/stage0/init/lean/parser/command.cpp
@@ -207,6 +207,7 @@ obj* l_Lean_Parser_command_include_HasView;
 obj* l_Lean_Parser_command_boolOptionValue_HasView_x_27___lambda__1(obj*);
 obj* l_RBNode_find___main___at_Lean_Parser_commandParser_run___spec__3___boxed(obj*);
 obj* l_Lean_Parser_command_variables_HasView_x_27___lambda__1(obj*);
+extern obj* l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens;
 extern obj* l_Lean_Parser_noKind;
 obj* l_Lean_Parser_command_setOption_HasView_x_27___lambda__1(obj*);
 obj* l_Lean_Parser_command_openSpec_renaming_HasView_x_27___lambda__1___closed__3;
@@ -264,8 +265,6 @@ obj* l_Lean_Parser_command_open;
 obj* l_Lean_Parser_command_openSpec_renaming_HasView_x_27___lambda__1___closed__1;
 obj* l_Lean_Parser_command_section_HasView;
 obj* l_Lean_Parser_command_namespace_Parser___closed__1;
-extern obj* l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens;
-obj* l_Lean_Parser_command_Declaration_Parser(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_end_HasView_x_27___lambda__1___closed__1;
 obj* l_RBNode_find___main___at_Lean_Parser_commandParser_run___spec__4___rarg___boxed(obj*, obj*);
 obj* l_Lean_Parser_number_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__3(obj*, obj*, obj*, obj*);
@@ -336,7 +335,6 @@ obj* l_Lean_Parser_command_attribute_Parser_Lean_Parser_HasTokens;
 obj* l_Lean_Parser_command_open_HasView_x_27___lambda__1___closed__3;
 obj* l_Option_toMonad___main___at_Lean_Parser_indexed___spec__2___rarg(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_optionValue_HasView;
-obj* l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1(obj*, obj*, obj*, obj*, obj*);
 obj* l_List_map___main___at_Lean_Parser_command_structBinderContent_HasView_x_27___elambda__1___spec__1(obj*);
 obj* l_RBNode_find___main___at_Lean_Parser_commandParser_run___spec__6(obj*);
 obj* l_Lean_Parser_Term_binder_Parser(obj*, obj*, obj*, obj*, obj*);
@@ -345,6 +343,7 @@ obj* l_Lean_Parser_stringLit_Parser___at_Lean_Parser_command_setOption_Parser_Le
 obj* l_Lean_Parser_command_attribute_Parser_Lean_Parser_HasView;
 obj* l_Lean_Parser_commandParser_run___lambda__1___boxed(obj*, obj*, obj*);
 obj* l_Lean_Parser_command_variable_HasView_x_27;
+obj* l_Lean_Parser_command_declaration_Parser(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_notation_Parser(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_setOption_Parser(obj*, obj*, obj*, obj*);
 extern obj* l_Lean_Parser_stringLit_HasView;
@@ -361,6 +360,7 @@ extern obj* l_Lean_Parser_command_mixfix_Parser_Lean_Parser_HasTokens;
 obj* l_RBNode_find___main___at_Lean_Parser_commandParser_run___spec__4(obj*);
 obj* l_Lean_Parser_command_setOption_HasView_x_27___lambda__1___closed__1;
 obj* l_Lean_Parser_command_omit_HasView_x_27___elambda__1(obj*);
+obj* l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_boolOptionValue_HasView;
 extern obj* l_Lean_Parser_Combinators_many___rarg___closed__1;
 obj* l_Lean_Parser_command_Parser_Lean_Parser_HasTokens;
@@ -4130,7 +4130,7 @@ lean::inc(x_28);
 x_31 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_31, 0, x_28);
 lean::cnstr_set(x_31, 1, x_14);
-x_32 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
+x_32 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
 lean::closure_set(x_32, 0, x_31);
 lean::inc(x_12);
 x_34 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_many___at_Lean_Parser_command_attrInstance_Parser_Lean_Parser_HasTokens___spec__2), 5, 1);
@@ -4180,7 +4180,7 @@ lean::inc(x_28);
 x_57 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_57, 0, x_28);
 lean::cnstr_set(x_57, 1, x_55);
-x_58 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
+x_58 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
 lean::closure_set(x_58, 0, x_57);
 x_59 = lean::mk_string("->");
 x_60 = l_String_trim(x_59);
@@ -4435,7 +4435,7 @@ lean::inc(x_24);
 x_27 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_27, 0, x_24);
 lean::cnstr_set(x_27, 1, x_10);
-x_28 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
+x_28 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
 lean::closure_set(x_28, 0, x_27);
 lean::inc(x_8);
 x_30 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_many___at_Lean_Parser_command_attrInstance_Parser_Lean_Parser_HasTokens___spec__2), 5, 1);
@@ -4485,7 +4485,7 @@ lean::inc(x_24);
 x_53 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_53, 0, x_24);
 lean::cnstr_set(x_53, 1, x_51);
-x_54 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
+x_54 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
 lean::closure_set(x_54, 0, x_53);
 x_55 = lean::mk_string("->");
 x_56 = l_String_trim(x_55);
@@ -10122,7 +10122,7 @@ lean::cnstr_set(x_21, 1, x_20);
 x_22 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_22, 0, x_13);
 lean::cnstr_set(x_22, 1, x_21);
-x_23 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
+x_23 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
 lean::closure_set(x_23, 0, x_22);
 x_24 = lean::mk_string("[");
 x_25 = l_String_trim(x_24);
@@ -10227,7 +10227,7 @@ lean::cnstr_set(x_17, 1, x_16);
 x_18 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_18, 0, x_9);
 lean::cnstr_set(x_18, 1, x_17);
-x_19 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
+x_19 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
 lean::closure_set(x_19, 0, x_18);
 x_20 = lean::mk_string("[");
 x_21 = l_String_trim(x_20);
@@ -12125,7 +12125,7 @@ return x_4;
 obj* _init_l_Lean_Parser_command_setOption_Parser_Lean_Parser_HasView() {
 _start:
 {
-obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; 
+obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; 
 x_0 = l_Lean_Parser_CommandParserM_Monad(lean::box(0));
 x_1 = l_Lean_Parser_CommandParserM_MonadExcept(lean::box(0));
 x_2 = l_Lean_Parser_CommandParserM_Lean_Parser_MonadParsec(lean::box(0));
@@ -12141,73 +12141,75 @@ x_10 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolCore___at
 lean::closure_set(x_10, 0, x_5);
 lean::closure_set(x_10, 1, x_9);
 lean::closure_set(x_10, 2, x_8);
-x_11 = lean::mk_string("True");
+x_11 = lean::mk_string("true");
 x_12 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolOrIdent___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__1___boxed), 5, 1);
 lean::closure_set(x_12, 0, x_11);
-x_13 = lean::box(0);
-lean::inc(x_12);
-x_15 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_15, 0, x_12);
-lean::cnstr_set(x_15, 1, x_13);
+x_13 = lean::mk_string("false");
+x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolOrIdent___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__1___boxed), 5, 1);
+lean::closure_set(x_14, 0, x_13);
+x_15 = lean::box(0);
 x_16 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_16, 0, x_12);
+lean::cnstr_set(x_16, 0, x_14);
 lean::cnstr_set(x_16, 1, x_15);
-x_17 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
-lean::closure_set(x_17, 0, x_16);
-lean::closure_set(x_17, 1, x_9);
-x_18 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_18, 0, x_17);
-lean::cnstr_set(x_18, 1, x_13);
-x_19 = l_Lean_Parser_command_boolOptionValue;
-x_20 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
-lean::closure_set(x_20, 0, x_19);
-lean::closure_set(x_20, 1, x_18);
-x_21 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_number_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__3___boxed), 4, 0);
-x_22 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_22, 0, x_21);
-lean::cnstr_set(x_22, 1, x_13);
-x_23 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_stringLit_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__2___boxed), 4, 0);
-x_24 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_24, 0, x_23);
-lean::cnstr_set(x_24, 1, x_22);
+x_17 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_17, 0, x_12);
+lean::cnstr_set(x_17, 1, x_16);
+x_18 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
+lean::closure_set(x_18, 0, x_17);
+lean::closure_set(x_18, 1, x_9);
+x_19 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_19, 0, x_18);
+lean::cnstr_set(x_19, 1, x_15);
+x_20 = l_Lean_Parser_command_boolOptionValue;
+x_21 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
+lean::closure_set(x_21, 0, x_20);
+lean::closure_set(x_21, 1, x_19);
+x_22 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_number_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__3___boxed), 4, 0);
+x_23 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_23, 0, x_22);
+lean::cnstr_set(x_23, 1, x_15);
+x_24 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_stringLit_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__2___boxed), 4, 0);
 x_25 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_25, 0, x_20);
-lean::cnstr_set(x_25, 1, x_24);
-x_26 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
-lean::closure_set(x_26, 0, x_25);
-lean::closure_set(x_26, 1, x_9);
-x_27 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_27, 0, x_26);
-lean::cnstr_set(x_27, 1, x_13);
-x_28 = l_Lean_Parser_command_optionValue;
-x_29 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
-lean::closure_set(x_29, 0, x_28);
-lean::closure_set(x_29, 1, x_27);
-x_30 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_30, 0, x_29);
-lean::cnstr_set(x_30, 1, x_13);
-x_31 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_ident_Parser___at_Lean_Parser_command_introRule_Parser_Lean_Parser_HasTokens___spec__1___boxed), 4, 0);
-x_32 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_32, 0, x_31);
-lean::cnstr_set(x_32, 1, x_30);
+lean::cnstr_set(x_25, 0, x_24);
+lean::cnstr_set(x_25, 1, x_23);
+x_26 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_26, 0, x_21);
+lean::cnstr_set(x_26, 1, x_25);
+x_27 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
+lean::closure_set(x_27, 0, x_26);
+lean::closure_set(x_27, 1, x_9);
+x_28 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_28, 0, x_27);
+lean::cnstr_set(x_28, 1, x_15);
+x_29 = l_Lean_Parser_command_optionValue;
+x_30 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
+lean::closure_set(x_30, 0, x_29);
+lean::closure_set(x_30, 1, x_28);
+x_31 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_31, 0, x_30);
+lean::cnstr_set(x_31, 1, x_15);
+x_32 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_ident_Parser___at_Lean_Parser_command_introRule_Parser_Lean_Parser_HasTokens___spec__1___boxed), 4, 0);
 x_33 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_33, 0, x_10);
-lean::cnstr_set(x_33, 1, x_32);
-x_34 = l_Lean_Parser_command_setOption;
-x_35 = l_Lean_Parser_command_setOption_HasView;
-x_36 = l_Lean_Parser_Combinators_node_view___rarg(x_0, x_1, x_2, x_3, x_34, x_33, x_35);
-lean::dec(x_33);
+lean::cnstr_set(x_33, 0, x_32);
+lean::cnstr_set(x_33, 1, x_31);
+x_34 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_34, 0, x_10);
+lean::cnstr_set(x_34, 1, x_33);
+x_35 = l_Lean_Parser_command_setOption;
+x_36 = l_Lean_Parser_command_setOption_HasView;
+x_37 = l_Lean_Parser_Combinators_node_view___rarg(x_0, x_1, x_2, x_3, x_35, x_34, x_36);
+lean::dec(x_34);
 lean::dec(x_3);
 lean::dec(x_2);
 lean::dec(x_1);
 lean::dec(x_0);
-return x_36;
+return x_37;
 }
 }
 obj* _init_l_Lean_Parser_command_setOption_Parser___closed__1() {
 _start:
 {
-obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; 
+obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; 
 x_0 = lean::mk_string("setOption");
 x_1 = l_String_trim(x_0);
 lean::dec(x_0);
@@ -12219,59 +12221,61 @@ x_6 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolCore___at_
 lean::closure_set(x_6, 0, x_1);
 lean::closure_set(x_6, 1, x_5);
 lean::closure_set(x_6, 2, x_4);
-x_7 = lean::mk_string("True");
+x_7 = lean::mk_string("true");
 x_8 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolOrIdent___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__1___boxed), 5, 1);
 lean::closure_set(x_8, 0, x_7);
-x_9 = lean::box(0);
-lean::inc(x_8);
-x_11 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_11, 0, x_8);
-lean::cnstr_set(x_11, 1, x_9);
+x_9 = lean::mk_string("false");
+x_10 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolOrIdent___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__1___boxed), 5, 1);
+lean::closure_set(x_10, 0, x_9);
+x_11 = lean::box(0);
 x_12 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_12, 0, x_8);
+lean::cnstr_set(x_12, 0, x_10);
 lean::cnstr_set(x_12, 1, x_11);
-x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
-lean::closure_set(x_13, 0, x_12);
-lean::closure_set(x_13, 1, x_5);
-x_14 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_14, 0, x_13);
-lean::cnstr_set(x_14, 1, x_9);
-x_15 = l_Lean_Parser_command_boolOptionValue;
-x_16 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
-lean::closure_set(x_16, 0, x_15);
-lean::closure_set(x_16, 1, x_14);
-x_17 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_number_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__3___boxed), 4, 0);
-x_18 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_18, 0, x_17);
-lean::cnstr_set(x_18, 1, x_9);
-x_19 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_stringLit_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__2___boxed), 4, 0);
-x_20 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_20, 0, x_19);
-lean::cnstr_set(x_20, 1, x_18);
+x_13 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_13, 0, x_8);
+lean::cnstr_set(x_13, 1, x_12);
+x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
+lean::closure_set(x_14, 0, x_13);
+lean::closure_set(x_14, 1, x_5);
+x_15 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_15, 0, x_14);
+lean::cnstr_set(x_15, 1, x_11);
+x_16 = l_Lean_Parser_command_boolOptionValue;
+x_17 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
+lean::closure_set(x_17, 0, x_16);
+lean::closure_set(x_17, 1, x_15);
+x_18 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_number_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__3___boxed), 4, 0);
+x_19 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_19, 0, x_18);
+lean::cnstr_set(x_19, 1, x_11);
+x_20 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_stringLit_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__2___boxed), 4, 0);
 x_21 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_21, 0, x_16);
-lean::cnstr_set(x_21, 1, x_20);
-x_22 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
-lean::closure_set(x_22, 0, x_21);
-lean::closure_set(x_22, 1, x_5);
-x_23 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_23, 0, x_22);
-lean::cnstr_set(x_23, 1, x_9);
-x_24 = l_Lean_Parser_command_optionValue;
-x_25 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
-lean::closure_set(x_25, 0, x_24);
-lean::closure_set(x_25, 1, x_23);
-x_26 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_26, 0, x_25);
-lean::cnstr_set(x_26, 1, x_9);
-x_27 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_ident_Parser___at_Lean_Parser_command_introRule_Parser_Lean_Parser_HasTokens___spec__1___boxed), 4, 0);
-x_28 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_28, 0, x_27);
-lean::cnstr_set(x_28, 1, x_26);
+lean::cnstr_set(x_21, 0, x_20);
+lean::cnstr_set(x_21, 1, x_19);
+x_22 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_22, 0, x_17);
+lean::cnstr_set(x_22, 1, x_21);
+x_23 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
+lean::closure_set(x_23, 0, x_22);
+lean::closure_set(x_23, 1, x_5);
+x_24 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_24, 0, x_23);
+lean::cnstr_set(x_24, 1, x_11);
+x_25 = l_Lean_Parser_command_optionValue;
+x_26 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
+lean::closure_set(x_26, 0, x_25);
+lean::closure_set(x_26, 1, x_24);
+x_27 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_27, 0, x_26);
+lean::cnstr_set(x_27, 1, x_11);
+x_28 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_ident_Parser___at_Lean_Parser_command_introRule_Parser_Lean_Parser_HasTokens___spec__1___boxed), 4, 0);
 x_29 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_29, 0, x_6);
-lean::cnstr_set(x_29, 1, x_28);
-return x_29;
+lean::cnstr_set(x_29, 0, x_28);
+lean::cnstr_set(x_29, 1, x_27);
+x_30 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_30, 0, x_6);
+lean::cnstr_set(x_30, 1, x_29);
+return x_30;
 }
 }
 obj* l_Lean_Parser_command_setOption_Parser(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
@@ -12366,7 +12370,7 @@ lean::dec(x_70);
 x_75 = l_Lean_Parser_command_variable_Parser_Lean_Parser_HasTokens;
 x_76 = l_Lean_Parser_tokenMapCons_tokens___rarg(x_75, x_73);
 lean::dec(x_73);
-x_78 = l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens;
+x_78 = l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens;
 x_79 = l_Lean_Parser_tokenMapCons_tokens___rarg(x_78, x_76);
 lean::dec(x_76);
 x_81 = l_Lean_Parser_tokenMapCons_tokens___rarg(x_78, x_79);
@@ -12409,7 +12413,7 @@ obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_5; obj* x_6; obj* x_7; obj* x_9;
 x_0 = lean::box(0);
 x_1 = lean::mk_string("/--");
 x_2 = lean_name_mk_string(x_0, x_1);
-x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser), 4, 0);
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser), 4, 0);
 lean::inc(x_3);
 x_5 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_5, 0, x_2);
diff --git a/src/stage0/init/lean/parser/declaration.cpp b/src/stage0/init/lean/parser/declaration.cpp
index 060d160e3e..f33ec934e7 100644
--- a/src/stage0/init/lean/parser/declaration.cpp
+++ b/src/stage0/init/lean/parser/declaration.cpp
@@ -51,14 +51,12 @@ obj* nat_sub(obj*, obj*);
 }
 obj* l_Lean_Parser_command_defLike_kind_HasView;
 obj* l_Lean_Parser_command_equation_HasView;
-obj* l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2(obj*);
 obj* l_Lean_Parser_command_identUnivParams_HasView_x_27___elambda__1(obj*);
 obj* l_Lean_Parser_command_declVal_HasView_x_27___lambda__1___closed__1;
 obj* l___private_init_lean_parser_token_4__ident_x_27(obj*, obj*, obj*);
 extern obj* l_Lean_Parser_Term_binderDefault_HasView;
 obj* l_Lean_Parser_command_structure_HasView_x_27___lambda__1___closed__6;
 obj* l_Lean_Parser_command_example_HasView_x_27;
-obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
 obj* l_Lean_Parser_command_declVal_Parser(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_visibility_HasView_x_27___lambda__1___closed__3;
 uint8 l_String_isEmpty(obj*);
@@ -70,12 +68,12 @@ obj* l_Lean_Parser_MonadParsec_strCore___at_Lean_Parser_command_docComment_Parse
 obj* l_Lean_Parser_command_univParams_HasView_x_27___lambda__1___closed__1;
 extern obj* l_Lean_Parser_Combinators_choiceAux___main___rarg___closed__1;
 obj* l_Lean_Parser_command_extends_HasView_x_27___lambda__1___closed__3;
+obj* l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1(obj*);
 obj* l_Lean_Parser_command_axiom_HasView_x_27;
 obj* l_Lean_Parser_command_declAttributes_HasView_x_27___lambda__1___closed__2;
 extern obj* l_Lean_Parser_Term_paren_HasView_x_27___elambda__1___closed__2;
 obj* l_Lean_Parser_command_oldUnivParams_Parser_Lean_Parser_HasView;
 obj* l_Lean_Parser_command_simpleDeclVal;
-obj* l_Lean_Parser_command_Declaration_inner;
 obj* l_Lean_Parser_Combinators_sepBy1_tokens___rarg(obj*, obj*);
 obj* l_Lean_Parser_command_declVal_HasView_x_27___lambda__1(obj*);
 obj* l_Lean_Parser_Term_Parser_Lean_Parser_HasTokens(obj*);
@@ -93,7 +91,6 @@ extern obj* l_Lean_Parser_finishCommentBlock___closed__2;
 obj* l_Lean_Parser_termParser_run(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_declModifiers_HasView_x_27___elambda__1___closed__1;
 obj* l_Lean_Parser_command_optDeclSig_Parser_Lean_Parser_HasView;
-obj* l_Lean_Parser_command_Declaration_Parser___closed__1;
 obj* l_Lean_Parser_command_defLike_HasView_x_27;
 obj* l_Lean_Parser_command_structureFieldBlock_Parser___closed__1;
 obj* l_Lean_Parser_command_structure_Parser(obj*, obj*, obj*, obj*);
@@ -133,6 +130,7 @@ obj* l_Lean_Parser_command_identUnivParams_HasView_x_27___lambda__1(obj*);
 obj* l_Lean_Parser_command_relaxedInferModifier_HasView_x_27;
 obj* l_Lean_Parser_MonadParsec_error___at___private_init_lean_parser_token_1__finishCommentBlockAux___main___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 extern obj* l_Lean_Parser_ident_Parser___at_Lean_Parser_command_NotationSpec_foldAction_Parser_Lean_Parser_HasTokens___spec__4___rarg___closed__1;
+obj* l_Lean_Parser_command_declaration_inner_HasView_x_27___elambda__1(obj*);
 obj* l_Lean_Parser_command_constantKeyword;
 obj* l_Lean_Parser_command_defLike;
 obj* l_Lean_Parser_command_structExplicitBinderContent_HasView;
@@ -166,6 +164,7 @@ obj* l_Lean_Parser_command_inferModifier_Parser_Lean_Parser_HasView___lambda__2(
 obj* l_Lean_Parser_command_inferModifier_Parser_Lean_Parser_HasView;
 obj* l_Lean_Parser_command_oldUnivParams;
 obj* l_Lean_Parser_command_structure_HasView_x_27___lambda__1___closed__2;
+obj* l_Lean_Parser_command_declaration_HasView_x_27___elambda__2(obj*);
 obj* l_Lean_Parser_command_axiom_HasView_x_27___elambda__2(obj*);
 obj* l_Lean_Parser_command_structBinderContent_Parser(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_structExplicitBinderContent_HasView_x_27;
@@ -174,12 +173,12 @@ obj* l_Lean_Parser_command_instance_HasView_x_27___lambda__1___closed__2;
 obj* l_Lean_Parser_command_simpleDeclVal_HasView_x_27___elambda__2___closed__1;
 obj* l_Lean_Parser_command_structureCtor_HasView;
 obj* l_Lean_Parser_withTrailing___at_Lean_Parser_token___spec__3(obj*, obj*, obj*, obj*);
-obj* l_Lean_Parser_command_Declaration_HasView_x_27;
 obj* l_Lean_Parser_command_visibility_HasView_x_27;
 obj* l_Lean_Parser_command_declAttributes_HasView_x_27___elambda__1(obj*);
 obj* l_Lean_Parser_command_instance_HasView_x_27;
 obj* l_Lean_Parser_command_declModifiers_HasView_x_27___lambda__1___closed__2;
 obj* l_Lean_Parser_command_axiom_HasView;
+obj* l_Lean_Parser_command_declaration_HasView;
 obj* l_Lean_Parser_Combinators_many___at_Lean_Parser_command_attrInstance_Parser_Lean_Parser_HasTokens___spec__2(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_declSig_Parser_Lean_Parser_HasTokens;
 extern obj* l_Lean_Parser_Level_leading_HasView_x_27___elambda__1___closed__3;
@@ -196,6 +195,7 @@ obj* l_Lean_Parser_command_declSig_Parser_Lean_Parser_HasView;
 obj* l_Lean_Parser_Syntax_asNode___main(obj*);
 obj* l_Lean_Parser_command_inferModifier_HasView;
 obj* l_Lean_Parser_command_inductive_HasView;
+obj* l_Lean_Parser_command_declaration_HasView_x_27;
 extern obj* l_Lean_Parser_detailIdentPartEscaped_HasView_x_27___elambda__1___closed__2;
 obj* l_Lean_Parser_command_attrInstance_HasView;
 obj* l_Lean_Parser_command_structure_HasView_x_27___lambda__1___closed__4;
@@ -216,6 +216,7 @@ obj* l_Lean_Parser_command_oldUnivParams_Parser_Lean_Parser_HasTokens;
 obj* l_Lean_Parser_command_optDeclSig_Parser(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_Term_Parser(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_declAttributes_HasView_x_27___lambda__1___closed__1;
+obj* l_Lean_Parser_command_declaration_inner_HasView;
 obj* l_Lean_Parser_command_declVal_HasView_x_27;
 extern obj* l_Lean_Parser_Term_binderContent_HasView_x_27___lambda__1___closed__1;
 obj* l_Lean_Parser_command_structureKw_HasView;
@@ -243,12 +244,14 @@ obj* string_append(obj*, obj*);
 obj* l_Lean_Parser_command_instImplicitBinder;
 obj* l_String_OldIterator_next___main(obj*);
 obj* l_Lean_Parser_command_declModifiers_HasView_x_27___lambda__1(obj*);
+obj* l_Lean_Parser_command_declaration_inner;
 obj* l_Lean_Parser_command_structBinderContent_HasView_x_27___lambda__1___closed__1;
 obj* l_Lean_Parser_command_attrInstance_Parser(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_defLike_kind_HasView_x_27___elambda__1___closed__3;
 extern obj* l___private_init_lean_parser_token_1__finishCommentBlockAux___main___closed__1;
 obj* l_Lean_Parser_command_inferModifier;
 obj* l_Lean_Parser_command_extends_HasView_x_27;
+obj* l_Lean_Parser_command_declaration_inner_HasView_x_27;
 obj* l_Lean_Parser_command_declModifiers_HasView_x_27___elambda__1(obj*);
 extern obj* l_Lean_Parser_command_notation_HasView_x_27___elambda__1___closed__1;
 obj* l_Lean_Parser_command_declModifiers_HasView;
@@ -262,7 +265,6 @@ obj* l_Lean_Parser_command_introRule_HasView_x_27___lambda__1(obj*);
 obj* l_Lean_Parser_command_strictImplicitBinder_HasView_x_27___elambda__1(obj*);
 obj* l_Lean_Parser_command_optDeclSig_HasView_x_27___lambda__1___closed__1;
 obj* l_Lean_Parser_command_identUnivParams_HasView_x_27___lambda__1___closed__5;
-obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27;
 obj* l_Lean_Parser_command_structImplicitBinder_HasView_x_27___elambda__1(obj*);
 obj* l_Lean_Parser_command_structBinderContent_Parser_Lean_Parser_HasTokens;
 obj* l_Lean_Parser_command_strictInferModifier_HasView;
@@ -271,6 +273,7 @@ extern obj* l_Char_HasRepr___closed__1;
 obj* l_List_mfoldl___main___at_Lean_Parser_command_docComment_Parser___spec__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_introRule_HasView_x_27___lambda__1___closed__1;
 obj* l_Lean_Parser_command_structBinderContent_HasView_x_27___elambda__1(obj*);
+obj* l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens;
 obj* l_Lean_Parser_command_declModifiers_Parser___closed__1;
 extern obj* l_Lean_Parser_noKind;
 obj* l_Lean_Parser_command_attrInstance_Parser_Lean_Parser_HasView;
@@ -320,6 +323,7 @@ obj* l_Lean_Parser_ParsecT_tryMkRes___rarg(obj*);
 obj* l_Lean_Parser_command_declSig_HasView_x_27___elambda__2___closed__2;
 obj* l_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens;
 obj* l_Lean_Parser_command_oldUnivParams_Parser(obj*, obj*, obj*, obj*);
+obj* l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__2;
 obj* l_Lean_Parser_command_relaxedInferModifier_HasView_x_27___elambda__1(obj*);
 obj* l_Lean_Parser_command_instance_HasView_x_27___lambda__1(obj*);
 obj* l_Lean_Parser_command_introRule_HasView_x_27___lambda__1___closed__2;
@@ -334,7 +338,6 @@ extern obj* l_Lean_Parser_Term_optType_Parser_Lean_Parser_HasTokens;
 obj* l_Lean_Parser_command_attrInstance;
 obj* l_ReaderT_lift___at_Lean_Parser_command_docComment_Parser_Lean_Parser_HasTokens___spec__8___boxed(obj*);
 obj* l_Lean_Parser_command_docComment_HasView_x_27___elambda__1___closed__1;
-obj* l_Lean_Parser_command_Declaration;
 obj* l_Lean_Parser_command_structExplicitBinderContent_HasView_x_27___lambda__1(obj*);
 obj* l_Lean_Parser_command_structureFieldBlock_Parser(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_identUnivParams_HasView_x_27___lambda__1___closed__2;
@@ -353,10 +356,8 @@ uint8 string_dec_eq(obj*, obj*);
 obj* l_Lean_Parser_command_declSig_HasView_x_27___elambda__2(obj*);
 obj* l_Lean_Parser_command_declSig_HasView_x_27;
 obj* l_Lean_Parser_command_docComment_HasView;
-obj* l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens;
 obj* l_Lean_Parser_command_visibility_HasView_x_27___lambda__1___closed__2;
 obj* l_Lean_Parser_command_identUnivParams_HasView_x_27___lambda__1___closed__3;
-obj* l_Lean_Parser_command_Declaration_Parser(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_structExplicitBinderContent_HasView_x_27___elambda__1(obj*);
 obj* l_Lean_Parser_command_instImplicitBinder_HasView;
 obj* l_Lean_Parser_command_declModifiers_HasView_x_27___lambda__1___closed__3;
@@ -376,7 +377,6 @@ obj* l_Lean_Parser_command_structureFieldBlock_HasView_x_27___lambda__1___closed
 obj* l_Lean_Parser_command_inferModifier_Parser_Lean_Parser_HasView___lambda__1(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_MonadParsec_strCore___at_Lean_Parser_command_docComment_Parser_Lean_Parser_HasTokens___spec__2(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_inferModifier_HasView_x_27___elambda__1(obj*);
-obj* l_Lean_Parser_command_Declaration_inner_HasView;
 obj* l_Lean_Parser_CommandParserM_Lean_Parser_MonadParsec(obj*);
 obj* l_Lean_Parser_command_declVal_Parser___closed__1;
 obj* l_Lean_Parser_command_relaxedInferModifier_HasView_x_27___lambda__1___closed__1;
@@ -386,6 +386,7 @@ obj* l_Lean_Parser_command_example_HasView_x_27___elambda__1(obj*);
 obj* l_Lean_Parser_command_equation_HasView_x_27___lambda__1(obj*);
 obj* l_Lean_Parser_command_defLike_kind_HasView_x_27___elambda__1___closed__1;
 obj* l_Lean_Parser_command_defLike_kind_HasView_x_27___elambda__1___closed__4;
+obj* l_Lean_Parser_command_declaration_HasView_x_27___elambda__1(obj*);
 obj* l_Lean_Parser_command_docComment_Parser(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_MonadParsec_error___at_Lean_Parser_command_docComment_Parser_Lean_Parser_HasTokens___spec__4___boxed(obj*);
 obj* l_Lean_Parser_command_declVal;
@@ -398,12 +399,13 @@ obj* l_String_trim(obj*);
 obj* l_Lean_Parser_command_axiom_HasView_x_27___elambda__2___closed__1;
 obj* l_Lean_Parser_ParsecT_bindMkRes___rarg(obj*, obj*);
 obj* l_Lean_Parser_command_declModifiers;
-obj* l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1;
 obj* l_Lean_Parser_command_structure_HasView;
 obj* l_Lean_Parser_command_declModifiers_HasView_x_27;
 extern obj* l_Lean_Parser_Term_binderDefault_Parser_Lean_Parser_HasTokens;
 obj* l_Lean_Parser_command_structureFieldBlock_HasView;
 extern obj* l_Lean_Parser_number_HasView_x_27___elambda__1___closed__6;
+obj* l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
+obj* l_Lean_Parser_command_declaration;
 obj* l_Lean_Parser_command_docComment_Parser_Lean_Parser_HasView___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l___private_init_lean_parser_combinators_2__sepByAux___main___at_Lean_Parser_command_declAttributes_Parser_Lean_Parser_HasTokens___spec__2(obj*, obj*, uint8, uint8, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_instance;
@@ -436,13 +438,13 @@ obj* l_Lean_Parser_command_constantKeyword_HasView;
 obj* l_Lean_Parser_command_docComment;
 obj* l_Lean_Parser_command_declVal_Parser_Lean_Parser_HasView;
 obj* l_Lean_Parser_command_structExplicitBinder_HasView_x_27___lambda__1___closed__3;
-obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27___elambda__1(obj*);
 obj* l_Lean_Parser_ParsecT_lookahead___at_Lean_Parser_command_docComment_Parser_Lean_Parser_HasView___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_Combinators_sepBy1___at_Lean_Parser_command_declAttributes_Parser_Lean_Parser_HasTokens___spec__1(obj*, obj*, uint8, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_structureFieldBlock_HasView_x_27;
 obj* l_Lean_Parser_MonadParsec_error___at_Lean_Parser_command_docComment_Parser_Lean_Parser_HasTokens___spec__4(obj*);
 extern obj* l_Lean_Parser_number_HasView_x_27___elambda__1___closed__4;
 obj* l___private_init_lean_parser_combinators_2__sepByAux___main___at_Lean_Parser_command_declAttributes_Parser_Lean_Parser_HasTokens___spec__2___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
+obj* l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1;
 obj* l_Lean_Parser_command_visibility_HasView_x_27___lambda__1(obj*);
 obj* l_Lean_Parser_command_defLike_kind;
 obj* l_Lean_Parser_command_attrInstance_HasView_x_27___elambda__1(obj*);
@@ -460,8 +462,9 @@ obj* l_Lean_Parser_command_attrInstance_Parser_Lean_Parser_HasTokens;
 obj* l_Lean_Parser_command_inferModifier_Parser_Lean_Parser_HasTokens;
 obj* l_Lean_Parser_command_constantKeyword_HasView_x_27;
 extern uint8 l_True_Decidable;
+obj* l_Lean_Parser_command_declaration_Parser___closed__1;
+obj* l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__2;
 obj* l_Lean_Parser_ident_Parser___at_Lean_Parser_command_introRule_Parser_Lean_Parser_HasTokens___spec__1(obj*, obj*, obj*, obj*);
-obj* l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__2;
 obj* l_Lean_Parser_command_declAttributes_HasView;
 obj* l_Lean_Parser_command_structImplicitBinder_HasView_x_27___lambda__1___closed__3;
 obj* l_Lean_Parser_command_univParams_HasView;
@@ -473,9 +476,7 @@ obj* l_Lean_Parser_command_docComment_HasView_x_27___elambda__1(obj*);
 obj* l_Lean_Parser_command_docComment_Parser_Lean_Parser_HasView___lambda__1(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_oldUnivParams_HasView_x_27;
 obj* l_Lean_Parser_command_optDeclSig_Parser_Lean_Parser_HasTokens;
-obj* l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_structureFieldBlock_Parser_Lean_Parser_HasTokens;
-obj* l_Lean_Parser_command_Declaration_HasView_x_27___elambda__1(obj*);
 extern obj* l_Lean_Parser_Term_typeSpec_HasView;
 obj* l_Lean_Parser_command_constantKeyword_HasView_x_27___lambda__1(obj*);
 obj* l_List_map___main___at_Lean_Parser_command_structBinderContent_HasView_x_27___elambda__1___spec__1(obj*);
@@ -490,13 +491,14 @@ obj* l_Lean_Parser_command_constantKeyword_HasView_x_27___lambda__1___closed__2;
 obj* l_Lean_Parser_command_defLike_HasView_x_27___elambda__1(obj*);
 obj* l_Lean_Parser_command_identUnivParams_HasView_x_27___lambda__1___closed__1;
 obj* l_Lean_Parser_command_introRule_Parser_Lean_Parser_HasView;
+obj* l_Lean_Parser_command_declaration_Parser(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_CommandParserM_Monad(obj*);
-obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__2;
 obj* l_Lean_Parser_command_structureCtor_HasView_x_27;
 obj* l_Lean_Parser_command_visibility_HasView_x_27___lambda__1___closed__4;
 obj* l_Lean_Parser_command_structure_HasView_x_27___lambda__1___closed__5;
 obj* l_Lean_Parser_command_optDeclSig_Parser___closed__1;
 obj* l_Lean_Parser_command_identUnivParams_Parser_Lean_Parser_HasTokens;
+obj* l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView;
 obj* l_Lean_Parser_command_defLike_kind_HasView_x_27___lambda__1___closed__2;
 obj* l_Lean_Parser_command_structExplicitBinder_HasView_x_27;
 obj* l_Lean_Parser_command_structureFieldBlock_HasView_x_27___lambda__1___closed__2;
@@ -506,9 +508,7 @@ obj* l_Lean_Parser_command_defLike_HasView_x_27___lambda__1___closed__2;
 obj* l_Lean_Parser_command_structExplicitBinderContent;
 obj* l_Lean_Parser_Term_typeSpec_Parser(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_Substring_ofString(obj*);
-obj* l_Lean_Parser_command_Declaration_HasView;
 obj* l_Lean_Parser_command_instance_HasView;
-obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1(obj*);
 obj* l_List_map___main___at_Lean_Parser_Term_tuple_HasView_x_27___elambda__1___spec__1(obj*);
 obj* l_Lean_Parser_command_oldUnivParams_HasView_x_27___lambda__1___closed__1;
 obj* l_Lean_Parser_command_optDeclSig_HasView;
@@ -517,6 +517,7 @@ obj* l_Lean_Parser_command_strictImplicitBinder_HasView_x_27___lambda__1(obj*);
 obj* l_Lean_Parser_command_structExplicitBinder_HasView_x_27___lambda__1___closed__1;
 obj* l_Lean_Parser_command_visibility;
 obj* l_Lean_Parser_command_structureKw_HasView_x_27___lambda__1(obj*);
+obj* l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_command_inductive_HasView_x_27;
 extern obj* l_Lean_Parser_Combinators_many___rarg___closed__1;
 obj* l_Lean_Parser_command_example;
@@ -543,7 +544,6 @@ obj* l_Lean_Parser_command_structureCtor_HasView_x_27___elambda__1(obj*);
 obj* l_Lean_Parser_command_constantKeyword_HasView_x_27___lambda__1___closed__1;
 obj* l_Lean_Parser_command_structExplicitBinder;
 extern obj* l_String_splitAux___main___closed__1;
-obj* l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView;
 namespace lean {
 obj* string_length(obj*);
 }
@@ -26230,7 +26230,7 @@ x_0 = l_Lean_Parser_command_inductive_HasView_x_27;
 return x_0;
 }
 }
-obj* _init_l_Lean_Parser_command_Declaration_inner() {
+obj* _init_l_Lean_Parser_command_declaration_inner() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; 
@@ -26241,14 +26241,14 @@ x_3 = lean::mk_string("Parser");
 x_4 = lean_name_mk_string(x_2, x_3);
 x_5 = lean::mk_string("command");
 x_6 = lean_name_mk_string(x_4, x_5);
-x_7 = lean::mk_string("Declaration");
+x_7 = lean::mk_string("declaration");
 x_8 = lean_name_mk_string(x_6, x_7);
 x_9 = lean::mk_string("inner");
 x_10 = lean_name_mk_string(x_8, x_9);
 return x_10;
 }
 }
-obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27___elambda__1(obj* x_0) {
+obj* l_Lean_Parser_command_declaration_inner_HasView_x_27___elambda__1(obj* x_0) {
 _start:
 {
 obj* x_1; 
@@ -26273,7 +26273,7 @@ x_12 = l_Lean_Parser_Syntax_mkNode(x_11, x_10);
 x_13 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_13, 0, x_12);
 lean::cnstr_set(x_13, 1, x_1);
-x_14 = l_Lean_Parser_command_Declaration_inner;
+x_14 = l_Lean_Parser_command_declaration_inner;
 x_15 = l_Lean_Parser_Syntax_mkNode(x_14, x_13);
 return x_15;
 }
@@ -26296,7 +26296,7 @@ x_26 = l_Lean_Parser_Syntax_mkNode(x_25, x_24);
 x_27 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_27, 0, x_26);
 lean::cnstr_set(x_27, 1, x_1);
-x_28 = l_Lean_Parser_command_Declaration_inner;
+x_28 = l_Lean_Parser_command_declaration_inner;
 x_29 = l_Lean_Parser_Syntax_mkNode(x_28, x_27);
 return x_29;
 }
@@ -26319,7 +26319,7 @@ x_40 = l_Lean_Parser_Syntax_mkNode(x_39, x_38);
 x_41 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_41, 0, x_40);
 lean::cnstr_set(x_41, 1, x_1);
-x_42 = l_Lean_Parser_command_Declaration_inner;
+x_42 = l_Lean_Parser_command_declaration_inner;
 x_43 = l_Lean_Parser_Syntax_mkNode(x_42, x_41);
 return x_43;
 }
@@ -26342,7 +26342,7 @@ x_54 = l_Lean_Parser_Syntax_mkNode(x_53, x_52);
 x_55 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_55, 0, x_54);
 lean::cnstr_set(x_55, 1, x_1);
-x_56 = l_Lean_Parser_command_Declaration_inner;
+x_56 = l_Lean_Parser_command_declaration_inner;
 x_57 = l_Lean_Parser_Syntax_mkNode(x_56, x_55);
 return x_57;
 }
@@ -26365,7 +26365,7 @@ x_68 = l_Lean_Parser_Syntax_mkNode(x_67, x_66);
 x_69 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_69, 0, x_68);
 lean::cnstr_set(x_69, 1, x_1);
-x_70 = l_Lean_Parser_command_Declaration_inner;
+x_70 = l_Lean_Parser_command_declaration_inner;
 x_71 = l_Lean_Parser_Syntax_mkNode(x_70, x_69);
 return x_71;
 }
@@ -26388,14 +26388,14 @@ x_82 = l_Lean_Parser_Syntax_mkNode(x_81, x_80);
 x_83 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_83, 0, x_82);
 lean::cnstr_set(x_83, 1, x_1);
-x_84 = l_Lean_Parser_command_Declaration_inner;
+x_84 = l_Lean_Parser_command_declaration_inner;
 x_85 = l_Lean_Parser_Syntax_mkNode(x_84, x_83);
 return x_85;
 }
 }
 }
 }
-obj* _init_l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1() {
+obj* _init_l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; 
@@ -26410,7 +26410,7 @@ lean::cnstr_set(x_6, 0, x_5);
 return x_6;
 }
 }
-obj* _init_l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__2() {
+obj* _init_l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__2() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; 
@@ -26421,14 +26421,14 @@ x_3 = lean::mk_string("Parser");
 x_4 = lean_name_mk_string(x_2, x_3);
 x_5 = lean::mk_string("command");
 x_6 = lean_name_mk_string(x_4, x_5);
-x_7 = lean::mk_string("Declaration");
+x_7 = lean::mk_string("declaration");
 x_8 = lean_name_mk_string(x_6, x_7);
 x_9 = lean::mk_string("inner");
 x_10 = lean_name_mk_string(x_8, x_9);
 return x_10;
 }
 }
-obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1(obj* x_0) {
+obj* l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1(obj* x_0) {
 _start:
 {
 obj* x_1; 
@@ -26436,7 +26436,7 @@ x_1 = l_Lean_Parser_Syntax_asNode___main(x_0);
 if (lean::obj_tag(x_1) == 0)
 {
 obj* x_2; 
-x_2 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
+x_2 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
 return x_2;
 }
 else
@@ -26450,14 +26450,14 @@ lean::inc(x_6);
 x_8 = lean::cnstr_get(x_3, 1);
 lean::inc(x_8);
 lean::dec(x_3);
-x_11 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__2;
+x_11 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__2;
 x_12 = lean_name_dec_eq(x_6, x_11);
 lean::dec(x_6);
 if (x_12 == 0)
 {
 obj* x_15; 
 lean::dec(x_8);
-x_15 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
+x_15 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
 return x_15;
 }
 else
@@ -26465,7 +26465,7 @@ else
 if (lean::obj_tag(x_8) == 0)
 {
 obj* x_16; 
-x_16 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
+x_16 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
 return x_16;
 }
 else
@@ -26483,7 +26483,7 @@ x_22 = l_Lean_Parser_Syntax_asNode___main(x_19);
 if (lean::obj_tag(x_22) == 0)
 {
 obj* x_23; 
-x_23 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
+x_23 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
 return x_23;
 }
 else
@@ -26499,7 +26499,7 @@ case 0:
 {
 obj* x_30; 
 lean::dec(x_24);
-x_30 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
+x_30 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
 return x_30;
 }
 case 1:
@@ -26507,7 +26507,7 @@ case 1:
 obj* x_33; 
 lean::dec(x_27);
 lean::dec(x_24);
-x_33 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
+x_33 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
 return x_33;
 }
 default:
@@ -26529,7 +26529,7 @@ if (x_43 == 0)
 obj* x_47; 
 lean::dec(x_34);
 lean::dec(x_39);
-x_47 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
+x_47 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
 return x_47;
 }
 else
@@ -26538,7 +26538,7 @@ if (lean::obj_tag(x_34) == 0)
 {
 obj* x_49; 
 lean::dec(x_39);
-x_49 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
+x_49 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
 return x_49;
 }
 else
@@ -26662,7 +26662,7 @@ obj* x_109;
 lean::dec(x_50);
 lean::dec(x_34);
 lean::dec(x_39);
-x_109 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
+x_109 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
 return x_109;
 }
 }
@@ -26676,7 +26676,7 @@ else
 obj* x_112; 
 lean::dec(x_8);
 lean::dec(x_17);
-x_112 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
+x_112 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
 return x_112;
 }
 }
@@ -26684,27 +26684,27 @@ return x_112;
 }
 }
 }
-obj* _init_l_Lean_Parser_command_Declaration_inner_HasView_x_27() {
+obj* _init_l_Lean_Parser_command_declaration_inner_HasView_x_27() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; 
-x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1), 1, 0);
-x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_inner_HasView_x_27___elambda__1), 1, 0);
+x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1), 1, 0);
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_inner_HasView_x_27___elambda__1), 1, 0);
 x_2 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_2, 0, x_0);
 lean::cnstr_set(x_2, 1, x_1);
 return x_2;
 }
 }
-obj* _init_l_Lean_Parser_command_Declaration_inner_HasView() {
+obj* _init_l_Lean_Parser_command_declaration_inner_HasView() {
 _start:
 {
 obj* x_0; 
-x_0 = l_Lean_Parser_command_Declaration_inner_HasView_x_27;
+x_0 = l_Lean_Parser_command_declaration_inner_HasView_x_27;
 return x_0;
 }
 }
-obj* _init_l_Lean_Parser_command_Declaration() {
+obj* _init_l_Lean_Parser_command_declaration() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; 
@@ -26715,12 +26715,12 @@ x_3 = lean::mk_string("Parser");
 x_4 = lean_name_mk_string(x_2, x_3);
 x_5 = lean::mk_string("command");
 x_6 = lean_name_mk_string(x_4, x_5);
-x_7 = lean::mk_string("Declaration");
+x_7 = lean::mk_string("declaration");
 x_8 = lean_name_mk_string(x_6, x_7);
 return x_8;
 }
 }
-obj* l_Lean_Parser_command_Declaration_HasView_x_27___elambda__1(obj* x_0) {
+obj* l_Lean_Parser_command_declaration_HasView_x_27___elambda__1(obj* x_0) {
 _start:
 {
 obj* x_1; obj* x_3; obj* x_6; obj* x_7; obj* x_10; obj* x_11; obj* x_12; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; 
@@ -26734,7 +26734,7 @@ x_7 = lean::cnstr_get(x_6, 1);
 lean::inc(x_7);
 lean::dec(x_6);
 x_10 = lean::apply_1(x_7, x_1);
-x_11 = l_Lean_Parser_command_Declaration_inner_HasView;
+x_11 = l_Lean_Parser_command_declaration_inner_HasView;
 x_12 = lean::cnstr_get(x_11, 1);
 lean::inc(x_12);
 lean::dec(x_11);
@@ -26746,12 +26746,12 @@ lean::cnstr_set(x_17, 1, x_16);
 x_18 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_18, 0, x_10);
 lean::cnstr_set(x_18, 1, x_17);
-x_19 = l_Lean_Parser_command_Declaration;
+x_19 = l_Lean_Parser_command_declaration;
 x_20 = l_Lean_Parser_Syntax_mkNode(x_19, x_18);
 return x_20;
 }
 }
-obj* _init_l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1() {
+obj* _init_l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_10; obj* x_11; 
@@ -26761,7 +26761,7 @@ lean::inc(x_1);
 lean::dec(x_0);
 x_4 = lean::box(3);
 x_5 = lean::apply_1(x_1, x_4);
-x_6 = l_Lean_Parser_command_Declaration_inner_HasView;
+x_6 = l_Lean_Parser_command_declaration_inner_HasView;
 x_7 = lean::cnstr_get(x_6, 0);
 lean::inc(x_7);
 lean::dec(x_6);
@@ -26772,11 +26772,11 @@ lean::cnstr_set(x_11, 1, x_10);
 return x_11;
 }
 }
-obj* _init_l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__2() {
+obj* _init_l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__2() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_4; obj* x_5; 
-x_0 = l_Lean_Parser_command_Declaration_inner_HasView;
+x_0 = l_Lean_Parser_command_declaration_inner_HasView;
 x_1 = lean::cnstr_get(x_0, 0);
 lean::inc(x_1);
 lean::dec(x_0);
@@ -26785,7 +26785,7 @@ x_5 = lean::apply_1(x_1, x_4);
 return x_5;
 }
 }
-obj* l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2(obj* x_0) {
+obj* l_Lean_Parser_command_declaration_HasView_x_27___elambda__2(obj* x_0) {
 _start:
 {
 obj* x_1; 
@@ -26793,7 +26793,7 @@ x_1 = l_Lean_Parser_Syntax_asNode___main(x_0);
 if (lean::obj_tag(x_1) == 0)
 {
 obj* x_2; 
-x_2 = l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1;
+x_2 = l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1;
 return x_2;
 }
 else
@@ -26808,7 +26808,7 @@ lean::dec(x_3);
 if (lean::obj_tag(x_6) == 0)
 {
 obj* x_9; 
-x_9 = l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1;
+x_9 = l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1;
 return x_9;
 }
 else
@@ -26827,7 +26827,7 @@ x_19 = lean::apply_1(x_16, x_10);
 if (lean::obj_tag(x_12) == 0)
 {
 obj* x_20; obj* x_21; 
-x_20 = l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__2;
+x_20 = l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__2;
 x_21 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_21, 0, x_19);
 lean::cnstr_set(x_21, 1, x_20);
@@ -26839,7 +26839,7 @@ obj* x_22; obj* x_25; obj* x_26; obj* x_29; obj* x_30;
 x_22 = lean::cnstr_get(x_12, 0);
 lean::inc(x_22);
 lean::dec(x_12);
-x_25 = l_Lean_Parser_command_Declaration_inner_HasView;
+x_25 = l_Lean_Parser_command_declaration_inner_HasView;
 x_26 = lean::cnstr_get(x_25, 0);
 lean::inc(x_26);
 lean::dec(x_25);
@@ -26853,27 +26853,27 @@ return x_30;
 }
 }
 }
-obj* _init_l_Lean_Parser_command_Declaration_HasView_x_27() {
+obj* _init_l_Lean_Parser_command_declaration_HasView_x_27() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; 
-x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2), 1, 0);
-x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_HasView_x_27___elambda__1), 1, 0);
+x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_HasView_x_27___elambda__2), 1, 0);
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_HasView_x_27___elambda__1), 1, 0);
 x_2 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_2, 0, x_0);
 lean::cnstr_set(x_2, 1, x_1);
 return x_2;
 }
 }
-obj* _init_l_Lean_Parser_command_Declaration_HasView() {
+obj* _init_l_Lean_Parser_command_declaration_HasView() {
 _start:
 {
 obj* x_0; 
-x_0 = l_Lean_Parser_command_Declaration_HasView_x_27;
+x_0 = l_Lean_Parser_command_declaration_HasView_x_27;
 return x_0;
 }
 }
-obj* _init_l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens() {
+obj* _init_l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; obj* x_4; obj* x_5; obj* x_7; obj* x_8; obj* x_10; obj* x_11; obj* x_13; obj* x_14; obj* x_16; obj* x_17; obj* x_19; obj* x_22; obj* x_25; obj* x_28; obj* x_31; obj* x_33; obj* x_35; obj* x_37; obj* x_38; obj* x_39; obj* x_40; obj* x_41; obj* x_42; obj* x_43; obj* x_44; obj* x_46; obj* x_48; obj* x_51; obj* x_53; obj* x_54; obj* x_56; obj* x_57; obj* x_58; obj* x_60; obj* x_62; obj* x_65; obj* x_67; obj* x_68; obj* x_70; obj* x_73; obj* x_75; obj* x_76; obj* x_78; obj* x_80; obj* x_82; obj* x_84; obj* x_86; obj* x_87; obj* x_89; obj* x_92; obj* x_94; obj* x_95; obj* x_97; obj* x_99; obj* x_100; obj* x_102; obj* x_104; obj* x_107; obj* x_109; obj* x_111; obj* x_112; obj* x_113; obj* x_115; obj* x_116; obj* x_117; obj* x_119; obj* x_122; obj* x_124; obj* x_126; obj* x_129; obj* x_132; obj* x_134; obj* x_135; obj* x_136; obj* x_139; obj* x_142; obj* x_145; obj* x_148; obj* x_151; obj* x_153; obj* x_155; obj* x_157; obj* x_159; obj* x_160; obj* x_162; 
@@ -27044,7 +27044,7 @@ lean::dec(x_160);
 return x_162;
 }
 }
-obj* l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+obj* l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
 obj* x_5; obj* x_6; obj* x_7; obj* x_9; obj* x_11; obj* x_12; obj* x_13; 
@@ -27071,7 +27071,7 @@ lean::cnstr_set(x_13, 1, x_9);
 return x_13;
 }
 }
-obj* _init_l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView() {
+obj* _init_l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; obj* x_39; obj* x_40; obj* x_41; obj* x_42; obj* x_43; obj* x_44; obj* x_45; uint8 x_46; obj* x_47; obj* x_49; obj* x_50; obj* x_51; obj* x_52; obj* x_55; obj* x_56; obj* x_58; obj* x_60; obj* x_61; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_68; obj* x_69; obj* x_72; obj* x_73; obj* x_75; obj* x_77; obj* x_78; obj* x_79; obj* x_80; obj* x_81; obj* x_82; obj* x_85; obj* x_86; obj* x_87; obj* x_88; obj* x_89; obj* x_90; obj* x_91; obj* x_94; obj* x_95; obj* x_96; obj* x_97; obj* x_98; obj* x_99; obj* x_100; obj* x_101; obj* x_103; obj* x_104; obj* x_105; obj* x_106; obj* x_107; obj* x_108; obj* x_111; obj* x_112; obj* x_114; obj* x_115; obj* x_116; obj* x_119; obj* x_120; obj* x_121; obj* x_122; obj* x_123; obj* x_124; obj* x_125; obj* x_126; obj* x_127; obj* x_128; obj* x_129; obj* x_130; obj* x_131; obj* x_132; obj* x_133; obj* x_134; obj* x_135; obj* x_136; obj* x_137; obj* x_138; obj* x_139; obj* x_140; obj* x_141; obj* x_142; obj* x_143; obj* x_144; obj* x_145; obj* x_146; obj* x_147; obj* x_148; obj* x_149; obj* x_150; obj* x_151; obj* x_152; obj* x_153; 
@@ -27304,7 +27304,7 @@ lean::cnstr_set(x_121, 1, x_35);
 x_122 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_122, 0, x_114);
 lean::cnstr_set(x_122, 1, x_121);
-x_123 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
+x_123 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
 lean::closure_set(x_123, 0, x_122);
 x_124 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_notationLike_Parser), 5, 0);
 x_125 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_termParser_run), 5, 1);
@@ -27362,7 +27362,7 @@ lean::closure_set(x_144, 1, x_9);
 x_145 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_145, 0, x_144);
 lean::cnstr_set(x_145, 1, x_35);
-x_146 = l_Lean_Parser_command_Declaration_inner;
+x_146 = l_Lean_Parser_command_declaration_inner;
 x_147 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
 lean::closure_set(x_147, 0, x_146);
 lean::closure_set(x_147, 1, x_145);
@@ -27373,8 +27373,8 @@ x_149 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declMo
 x_150 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_150, 0, x_149);
 lean::cnstr_set(x_150, 1, x_148);
-x_151 = l_Lean_Parser_command_Declaration;
-x_152 = l_Lean_Parser_command_Declaration_HasView;
+x_151 = l_Lean_Parser_command_declaration;
+x_152 = l_Lean_Parser_command_declaration_HasView;
 x_153 = l_Lean_Parser_Combinators_node_view___rarg(x_0, x_1, x_2, x_3, x_151, x_150, x_152);
 lean::dec(x_150);
 lean::dec(x_3);
@@ -27384,7 +27384,7 @@ lean::dec(x_0);
 return x_153;
 }
 }
-obj* _init_l_Lean_Parser_command_Declaration_Parser___closed__1() {
+obj* _init_l_Lean_Parser_command_declaration_Parser___closed__1() {
 _start:
 {
 obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_29; obj* x_30; obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; obj* x_39; obj* x_40; obj* x_41; uint8 x_42; obj* x_43; obj* x_45; obj* x_46; obj* x_47; obj* x_48; obj* x_51; obj* x_52; obj* x_54; obj* x_56; obj* x_57; obj* x_58; obj* x_59; obj* x_60; obj* x_61; obj* x_64; obj* x_65; obj* x_68; obj* x_69; obj* x_71; obj* x_73; obj* x_74; obj* x_75; obj* x_76; obj* x_77; obj* x_78; obj* x_81; obj* x_82; obj* x_83; obj* x_84; obj* x_85; obj* x_86; obj* x_87; obj* x_90; obj* x_91; obj* x_92; obj* x_93; obj* x_94; obj* x_95; obj* x_96; obj* x_97; obj* x_99; obj* x_100; obj* x_101; obj* x_102; obj* x_103; obj* x_104; obj* x_107; obj* x_108; obj* x_110; obj* x_111; obj* x_112; obj* x_115; obj* x_116; obj* x_117; obj* x_118; obj* x_119; obj* x_120; obj* x_121; obj* x_122; obj* x_123; obj* x_124; obj* x_125; obj* x_126; obj* x_127; obj* x_128; obj* x_129; obj* x_130; obj* x_131; obj* x_132; obj* x_133; obj* x_134; obj* x_135; obj* x_136; obj* x_137; obj* x_138; obj* x_139; obj* x_140; obj* x_141; obj* x_142; obj* x_143; obj* x_144; obj* x_145; obj* x_146; 
@@ -27613,7 +27613,7 @@ lean::cnstr_set(x_117, 1, x_31);
 x_118 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_118, 0, x_110);
 lean::cnstr_set(x_118, 1, x_117);
-x_119 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
+x_119 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
 lean::closure_set(x_119, 0, x_118);
 x_120 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_notationLike_Parser), 5, 0);
 x_121 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_termParser_run), 5, 1);
@@ -27671,7 +27671,7 @@ lean::closure_set(x_140, 1, x_5);
 x_141 = lean::alloc_cnstr(1, 2, 0);
 lean::cnstr_set(x_141, 0, x_140);
 lean::cnstr_set(x_141, 1, x_31);
-x_142 = l_Lean_Parser_command_Declaration_inner;
+x_142 = l_Lean_Parser_command_declaration_inner;
 x_143 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
 lean::closure_set(x_143, 0, x_142);
 lean::closure_set(x_143, 1, x_141);
@@ -27685,12 +27685,12 @@ lean::cnstr_set(x_146, 1, x_144);
 return x_146;
 }
 }
-obj* l_Lean_Parser_command_Declaration_Parser(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+obj* l_Lean_Parser_command_declaration_Parser(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 obj* x_4; obj* x_5; obj* x_6; 
-x_4 = l_Lean_Parser_command_Declaration;
-x_5 = l_Lean_Parser_command_Declaration_Parser___closed__1;
+x_4 = l_Lean_Parser_command_declaration;
+x_5 = l_Lean_Parser_command_declaration_Parser___closed__1;
 x_6 = l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2(x_4, x_5, x_0, x_1, x_2, x_3);
 return x_6;
 }
@@ -28229,31 +28229,31 @@ lean::mark_persistent(l_Lean_Parser_command_inductive_HasView_x_27___lambda__1__
 lean::mark_persistent(l_Lean_Parser_command_inductive_HasView_x_27);
  l_Lean_Parser_command_inductive_HasView = _init_l_Lean_Parser_command_inductive_HasView();
 lean::mark_persistent(l_Lean_Parser_command_inductive_HasView);
- l_Lean_Parser_command_Declaration_inner = _init_l_Lean_Parser_command_Declaration_inner();
-lean::mark_persistent(l_Lean_Parser_command_Declaration_inner);
- l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1 = _init_l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1();
-lean::mark_persistent(l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1);
- l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__2 = _init_l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__2();
-lean::mark_persistent(l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__2);
- l_Lean_Parser_command_Declaration_inner_HasView_x_27 = _init_l_Lean_Parser_command_Declaration_inner_HasView_x_27();
-lean::mark_persistent(l_Lean_Parser_command_Declaration_inner_HasView_x_27);
- l_Lean_Parser_command_Declaration_inner_HasView = _init_l_Lean_Parser_command_Declaration_inner_HasView();
-lean::mark_persistent(l_Lean_Parser_command_Declaration_inner_HasView);
- l_Lean_Parser_command_Declaration = _init_l_Lean_Parser_command_Declaration();
-lean::mark_persistent(l_Lean_Parser_command_Declaration);
- l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1 = _init_l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1();
-lean::mark_persistent(l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1);
- l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__2 = _init_l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__2();
-lean::mark_persistent(l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__2);
- l_Lean_Parser_command_Declaration_HasView_x_27 = _init_l_Lean_Parser_command_Declaration_HasView_x_27();
-lean::mark_persistent(l_Lean_Parser_command_Declaration_HasView_x_27);
- l_Lean_Parser_command_Declaration_HasView = _init_l_Lean_Parser_command_Declaration_HasView();
-lean::mark_persistent(l_Lean_Parser_command_Declaration_HasView);
- l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens = _init_l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens();
-lean::mark_persistent(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens);
- l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView = _init_l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView();
-lean::mark_persistent(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView);
- l_Lean_Parser_command_Declaration_Parser___closed__1 = _init_l_Lean_Parser_command_Declaration_Parser___closed__1();
-lean::mark_persistent(l_Lean_Parser_command_Declaration_Parser___closed__1);
+ l_Lean_Parser_command_declaration_inner = _init_l_Lean_Parser_command_declaration_inner();
+lean::mark_persistent(l_Lean_Parser_command_declaration_inner);
+ l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1 = _init_l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1();
+lean::mark_persistent(l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1);
+ l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__2 = _init_l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__2();
+lean::mark_persistent(l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__2);
+ l_Lean_Parser_command_declaration_inner_HasView_x_27 = _init_l_Lean_Parser_command_declaration_inner_HasView_x_27();
+lean::mark_persistent(l_Lean_Parser_command_declaration_inner_HasView_x_27);
+ l_Lean_Parser_command_declaration_inner_HasView = _init_l_Lean_Parser_command_declaration_inner_HasView();
+lean::mark_persistent(l_Lean_Parser_command_declaration_inner_HasView);
+ l_Lean_Parser_command_declaration = _init_l_Lean_Parser_command_declaration();
+lean::mark_persistent(l_Lean_Parser_command_declaration);
+ l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1 = _init_l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1();
+lean::mark_persistent(l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1);
+ l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__2 = _init_l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__2();
+lean::mark_persistent(l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__2);
+ l_Lean_Parser_command_declaration_HasView_x_27 = _init_l_Lean_Parser_command_declaration_HasView_x_27();
+lean::mark_persistent(l_Lean_Parser_command_declaration_HasView_x_27);
+ l_Lean_Parser_command_declaration_HasView = _init_l_Lean_Parser_command_declaration_HasView();
+lean::mark_persistent(l_Lean_Parser_command_declaration_HasView);
+ l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens = _init_l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens();
+lean::mark_persistent(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens);
+ l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView = _init_l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView();
+lean::mark_persistent(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView);
+ l_Lean_Parser_command_declaration_Parser___closed__1 = _init_l_Lean_Parser_command_declaration_Parser___closed__1();
+lean::mark_persistent(l_Lean_Parser_command_declaration_Parser___closed__1);
 return w;
 }
diff --git a/src/util/object_ref.h b/src/util/object_ref.h
index 40d4c9c3dc..8301175f4d 100644
--- a/src/util/object_ref.h
+++ b/src/util/object_ref.h
@@ -35,7 +35,7 @@ public:
     }
     object * raw() const { return m_obj; }
     object * steal() { object * r = m_obj; m_obj = box(0); return r; }
-    object * get() const { inc(m_obj); return m_obj; }
+    object * get_obj_arg() const { inc(m_obj); return m_obj; }
     static void swap(object_ref & a, object_ref & b) { std::swap(a.m_obj, b.m_obj); }
 };