diff --git a/library/init/lean/elaborator/command.lean b/library/init/lean/elaborator/command.lean
index 56d0091877..1f77747ccf 100644
--- a/library/init/lean/elaborator/command.lean
+++ b/library/init/lean/elaborator/command.lean
@@ -7,6 +7,7 @@ prelude
 import init.lean.elaborator.alias
 import init.lean.elaborator.basic
 import init.lean.elaborator.resolvename
+import init.lean.elaborator.preterm
 
 namespace Lean
 namespace Elab
@@ -195,6 +196,13 @@ fun n => do
   runIO (IO.println (toString pos ++ " " ++ toString resolvedIds));
   pure ()
 
+@[builtinCommandElab «preterm»] def elabPreTerm : CommandElab :=
+fun n => do
+  let s := n.getArg 1;
+  pre ← toPreTerm s;
+  runIO (IO.println pre.dbgToString);
+  pure ()
+
 /- We just ignore Lean3 notation declaration commands. -/
 @[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()
 @[builtinCommandElab «reserve»] def elabReserve : CommandElab := fun _ => pure ()
diff --git a/library/init/lean/elaborator/preterm.lean b/library/init/lean/elaborator/preterm.lean
index a6198e9a20..548eef611a 100644
--- a/library/init/lean/elaborator/preterm.lean
+++ b/library/init/lean/elaborator/preterm.lean
@@ -26,7 +26,7 @@ do m ← builtinPreTermElabTable.get;
    builtinPreTermElabTable.modify $ fun m => m.insert k elab
 
 def declareBuiltinPreTermElab (env : Environment) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
-declareBuiltinElab env `Lean.addBuiltinTermElab kind declName
+declareBuiltinElab env `Lean.addBuiltinPreTermElab kind declName
 
 @[init] def registerBuiltinPreTermElabAttr : IO Unit :=
 registerAttribute {
@@ -45,4 +45,29 @@ registerAttribute {
  applicationTime := AttributeApplicationTime.afterCompilation
 }
 
+def Expr.mkAnnotation (ann : Name) (e : Expr) :=
+Expr.mdata (MData.empty.setName `annotation ann) e
+
+private def dummy : Expr := Expr.const `Prop []
+
+namespace Elab
+
+def toPreTerm (stx : Syntax) : Elab PreTerm :=
+stx.ifNode
+  (fun n => do
+    s ← get;
+    table ← runIO builtinPreTermElabTable.get;
+    let k      := n.getKind;
+    match table.find k with
+    | some fn => fn n
+    | none    => logErrorAndThrow stx ("`toPreTerm` failed, no support for syntax '" ++ toString k ++ "'"))
+  (fun _ => throw "`toPreTerm` failed, unexpected syntax")
+
+@[builtinPreTermElab «type»] def convertType : PreTermElab :=
+fun _ => pure $ Expr.sort $ Level.succ Level.zero
+
+@[builtinPreTermElab «sort»] def convertSort : PreTermElab :=
+fun _ => pure $ Expr.sort Level.zero
+
+end Elab
 end Lean
diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean
index 2f63d08997..c6c39ddd89 100644
--- a/library/init/lean/parser/command.lean
+++ b/library/init/lean/parser/command.lean
@@ -82,6 +82,7 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
 @[builtinCommandParser] def check          := parser! "#check " >> termParser
 @[builtinCommandParser] def exit           := parser! "#exit"
 @[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
+@[builtinCommandParser] def «preterm»      := parser! "#preterm " >> termParser
 @[builtinCommandParser] def «init_quot»    := parser! "init_quot"
 @[builtinCommandParser] def «set_option»   := parser! "set_option " >> ident >> (symbolOrIdent "true" <|> symbolOrIdent "false" <|> strLit <|> numLit)
 @[builtinCommandParser] def «attribute»    := parser! optional "local " >> "attribute " >> "[" >> sepBy1 attrInstance ", " >> "]" >> many1 ident
diff --git a/src/stage0/init/lean/elaborator/command.cpp b/src/stage0/init/lean/elaborator/command.cpp
index bfb95171bb..349d626e69 100644
--- a/src/stage0/init/lean/elaborator/command.cpp
+++ b/src/stage0/init/lean/elaborator/command.cpp
@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.elaborator.command
-// Imports: init.lean.elaborator.alias init.lean.elaborator.basic init.lean.elaborator.resolvename
+// Imports: init.lean.elaborator.alias init.lean.elaborator.basic init.lean.elaborator.resolvename init.lean.elaborator.preterm
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -44,6 +44,7 @@ obj* l_Lean_Elab_elabOpen(obj*, obj*, obj*);
 obj* l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__2;
 extern obj* l_Lean_Parser_Command_export___elambda__1___closed__2;
 obj* l_List_lengthAux___main___rarg(obj*, obj*);
+extern "C" obj* lean_expr_dbg_to_string(obj*);
 obj* l___regBuiltinTermElab_Lean_Elab_elabNotation___closed__1;
 obj* l_Lean_Elab_elabEnd___closed__4;
 obj* l___regBuiltinTermElab_Lean_Elab_elabUniverse___closed__2;
@@ -78,6 +79,7 @@ obj* l___regBuiltinTermElab_Lean_Elab_elabOpen___closed__3;
 obj* l_Lean_Name_toStringWithSep___main(obj*, obj*);
 obj* l___regBuiltinTermElab_Lean_Elab_elabUniverse(obj*);
 obj* l___regBuiltinTermElab_Lean_Elab_elabUniverse___closed__3;
+extern obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
 obj* l_Lean_Elab_addUniverse___closed__1;
 obj* l_Lean_Elab_elabOpenOnly___boxed(obj*, obj*, obj*);
 obj* l_Lean_Elab_addUniverse(obj*, obj*, obj*);
@@ -104,7 +106,6 @@ extern obj* l_List_repr___rarg___closed__2;
 obj* l_Lean_Elab_getNamespace___rarg(obj*);
 obj* l_Lean_Elab_elabOpenRenaming(obj*, obj*, obj*);
 extern obj* l_Lean_Parser_Command_mixfix___elambda__1___closed__2;
-obj* l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__5;
 extern obj* l_Lean_Parser_Command_openHiding___elambda__1___closed__2;
 obj* l_Lean_addAlias(obj*, obj*, obj*);
 extern obj* l_Lean_Parser_Command_universes___elambda__1___closed__2;
@@ -159,6 +160,7 @@ obj* l_Lean_Elab_elabEnd___closed__6;
 uint8 l_Lean_Name_eqStr(obj*, obj*);
 uint8 l_List_elem___main___at_Lean_Parser_addBuiltinLeadingParser___spec__4(obj*, obj*);
 obj* l_Lean_Elab_elabUniverses___boxed(obj*, obj*, obj*);
+obj* l_Lean_Elab_elabPreTerm___boxed(obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Lean_Elab_elabExport___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 extern obj* l_Sigma_HasRepr___rarg___closed__2;
 obj* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Elab_elabOpenHiding___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
@@ -176,11 +178,12 @@ obj* l___regBuiltinTermElab_Lean_Elab_elabResolveName___closed__1;
 obj* l_Lean_logUnknownDecl(obj*, obj*, obj*, obj*);
 obj* l_List_toString___at_Lean_Elab_elabResolveName___spec__1(obj*);
 obj* l_Lean_Elab_elabEnd(obj*, obj*, obj*);
+obj* l_Lean_Elab_toPreTerm(obj*, obj*, obj*);
 obj* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Elab_elabUniverses___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Elab_elabEnd___closed__5;
 obj* l_Array_size(obj*, obj*);
 extern obj* l_Lean_Parser_Command_section___elambda__1___rarg___closed__2;
-obj* l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__4;
+obj* l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__2;
 obj* l_Array_get(obj*, obj*, obj*, obj*);
 obj* l___regBuiltinTermElab_Lean_Elab_elabNotation___closed__2;
 obj* l___regBuiltinTermElab_Lean_Elab_elabExport(obj*);
@@ -191,7 +194,7 @@ obj* l___regBuiltinTermElab_Lean_Elab_elabInitQuot___closed__2;
 obj* l___regBuiltinTermElab_Lean_Elab_elabNamespace(obj*);
 obj* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Elab_elabOpenSimple___spec__1(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l___regBuiltinTermElab_Lean_Elab_elabSection___closed__1;
-extern obj* l_Lean_nameToExprAux___main___closed__4;
+obj* l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__3;
 extern obj* l_Lean_Name_toString___closed__1;
 obj* l___private_init_lean_elaborator_command_4__checkEndHeader___boxed(obj*, obj*);
 uint8 l_Lean_Environment_contains(obj*, obj*);
@@ -207,9 +210,12 @@ extern obj* l_Lean_Parser_Command_reserve___elambda__1___closed__2;
 obj* l___regBuiltinTermElab_Lean_Elab_elabEnd___closed__1;
 obj* l_Lean_Elab_elabInitQuot___boxed(obj*);
 obj* l_Lean_Elab_elabMixfix(obj*, obj*);
+obj* l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__1;
 uint8 l___private_init_lean_elaborator_command_4__checkEndHeader(obj*, obj*);
 obj* l_Lean_Elab_elabOpenHiding___boxed(obj*, obj*, obj*);
+obj* l_Lean_Elab_elabPreTerm(obj*, obj*, obj*);
 obj* l_Lean_Elab_elabNotation(obj*, obj*);
+obj* l___regBuiltinTermElab_Lean_Elab_elabPreTerm(obj*);
 obj* l_Lean_Elab_modifyScope___boxed(obj*, obj*, obj*);
 obj* l_Lean_Elab_elabReserve(obj*, obj*);
 obj* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Elab_elabOpenSimple___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
@@ -221,6 +227,7 @@ obj* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Elab_elabOpenRenaming___spec__1
 obj* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Elab_elabOpenOnly___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__3;
 extern obj* l_Lean_Parser_Command_universe___elambda__1___rarg___closed__2;
+extern obj* l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 obj* l_Lean_Elab_elabUniverse(obj*, obj*, obj*);
 obj* l_Lean_Elab_modifyScope___at_Lean_Elab_addUniverse___spec__1(obj*, obj*, obj*);
 extern obj* l_List_repr___rarg___closed__1;
@@ -801,7 +808,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__1() {
 _start:
 {
 obj* x_1; 
-x_1 = lean::mk_string("Elab");
+x_1 = lean::mk_string("elabNamespace");
 return x_1;
 }
 }
@@ -809,7 +816,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2() {
 _start:
 {
 obj* x_1; obj* x_2; obj* x_3; 
-x_1 = l_Lean_nameToExprAux___main___closed__4;
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 x_2 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -819,24 +826,6 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__3() {
 _start:
 {
 obj* x_1; 
-x_1 = lean::mk_string("elabNamespace");
-return x_1;
-}
-}
-obj* _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__4() {
-_start:
-{
-obj* x_1; obj* x_2; obj* x_3; 
-x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
-x_2 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__3;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-obj* _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__5() {
-_start:
-{
-obj* x_1; 
 x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elab_elabNamespace___boxed), 3, 0);
 return x_1;
 }
@@ -846,8 +835,8 @@ _start:
 {
 obj* x_2; obj* x_3; obj* x_4; obj* x_5; 
 x_2 = l_Lean_Parser_Command_namespace___elambda__1___rarg___closed__2;
-x_3 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__4;
-x_4 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__5;
+x_3 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
+x_4 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__3;
 x_5 = l_Lean_addBuiltinCommandElab(x_2, x_3, x_4, x_1);
 return x_5;
 }
@@ -1160,7 +1149,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabSection___closed__2() {
 _start:
 {
 obj* x_1; obj* x_2; obj* x_3; 
-x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 x_2 = l___regBuiltinTermElab_Lean_Elab_elabSection___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -1746,7 +1735,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabEnd___closed__2() {
 _start:
 {
 obj* x_1; obj* x_2; obj* x_3; 
-x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 x_2 = l___regBuiltinTermElab_Lean_Elab_elabEnd___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -2759,7 +2748,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabExport___closed__2() {
 _start:
 {
 obj* x_1; obj* x_2; obj* x_3; 
-x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 x_2 = l___regBuiltinTermElab_Lean_Elab_elabExport___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -5234,7 +5223,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabOpen___closed__2() {
 _start:
 {
 obj* x_1; obj* x_2; obj* x_3; 
-x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 x_2 = l___regBuiltinTermElab_Lean_Elab_elabOpen___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -5839,7 +5828,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabUniverse___closed__2() {
 _start:
 {
 obj* x_1; obj* x_2; obj* x_3; 
-x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 x_2 = l___regBuiltinTermElab_Lean_Elab_elabUniverse___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -6016,7 +6005,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabUniverses___closed__2() {
 _start:
 {
 obj* x_1; obj* x_2; obj* x_3; 
-x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 x_2 = l___regBuiltinTermElab_Lean_Elab_elabUniverses___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -6177,7 +6166,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabInitQuot___closed__2() {
 _start:
 {
 obj* x_1; obj* x_2; obj* x_3; 
-x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 x_2 = l___regBuiltinTermElab_Lean_Elab_elabInitQuot___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -6711,7 +6700,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabResolveName___closed__2() {
 _start:
 {
 obj* x_1; obj* x_2; obj* x_3; 
-x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 x_2 = l___regBuiltinTermElab_Lean_Elab_elabResolveName___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -6736,6 +6725,216 @@ x_5 = l_Lean_addBuiltinCommandElab(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
+obj* l_Lean_Elab_elabPreTerm(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; 
+x_4 = lean::cnstr_get(x_1, 1);
+x_5 = lean::box(0);
+x_6 = lean::mk_nat_obj(1u);
+x_7 = lean::array_get(x_5, x_4, x_6);
+lean::inc(x_2);
+x_8 = l_Lean_Elab_toPreTerm(x_7, x_2, x_3);
+if (lean::obj_tag(x_8) == 0)
+{
+uint8 x_9; 
+x_9 = !lean::is_exclusive(x_8);
+if (x_9 == 0)
+{
+obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; 
+x_10 = lean::cnstr_get(x_8, 0);
+x_11 = lean::box(0);
+lean::cnstr_set(x_8, 0, x_11);
+x_12 = lean_expr_dbg_to_string(x_10);
+lean::dec(x_10);
+x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_IO_println___at_HasRepr_HasEval___spec__1___boxed), 2, 1);
+lean::closure_set(x_13, 0, x_12);
+x_14 = l_Lean_Elab_runIOUnsafe___rarg(x_13, x_2, x_8);
+lean::dec(x_2);
+if (lean::obj_tag(x_14) == 0)
+{
+uint8 x_15; 
+x_15 = !lean::is_exclusive(x_14);
+if (x_15 == 0)
+{
+obj* x_16; 
+x_16 = lean::cnstr_get(x_14, 0);
+lean::dec(x_16);
+lean::cnstr_set(x_14, 0, x_11);
+return x_14;
+}
+else
+{
+obj* x_17; obj* x_18; 
+x_17 = lean::cnstr_get(x_14, 1);
+lean::inc(x_17);
+lean::dec(x_14);
+x_18 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_18, 0, x_11);
+lean::cnstr_set(x_18, 1, x_17);
+return x_18;
+}
+}
+else
+{
+uint8 x_19; 
+x_19 = !lean::is_exclusive(x_14);
+if (x_19 == 0)
+{
+return x_14;
+}
+else
+{
+obj* x_20; obj* x_21; obj* x_22; 
+x_20 = lean::cnstr_get(x_14, 0);
+x_21 = lean::cnstr_get(x_14, 1);
+lean::inc(x_21);
+lean::inc(x_20);
+lean::dec(x_14);
+x_22 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_22, 0, x_20);
+lean::cnstr_set(x_22, 1, x_21);
+return x_22;
+}
+}
+}
+else
+{
+obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; 
+x_23 = lean::cnstr_get(x_8, 0);
+x_24 = lean::cnstr_get(x_8, 1);
+lean::inc(x_24);
+lean::inc(x_23);
+lean::dec(x_8);
+x_25 = lean::box(0);
+x_26 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_26, 0, x_25);
+lean::cnstr_set(x_26, 1, x_24);
+x_27 = lean_expr_dbg_to_string(x_23);
+lean::dec(x_23);
+x_28 = lean::alloc_closure(reinterpret_cast<void*>(l_IO_println___at_HasRepr_HasEval___spec__1___boxed), 2, 1);
+lean::closure_set(x_28, 0, x_27);
+x_29 = l_Lean_Elab_runIOUnsafe___rarg(x_28, x_2, x_26);
+lean::dec(x_2);
+if (lean::obj_tag(x_29) == 0)
+{
+obj* x_30; obj* x_31; obj* x_32; 
+x_30 = lean::cnstr_get(x_29, 1);
+lean::inc(x_30);
+if (lean::is_exclusive(x_29)) {
+ lean::cnstr_release(x_29, 0);
+ lean::cnstr_release(x_29, 1);
+ x_31 = x_29;
+} else {
+ lean::dec_ref(x_29);
+ x_31 = lean::box(0);
+}
+if (lean::is_scalar(x_31)) {
+ x_32 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_32 = x_31;
+}
+lean::cnstr_set(x_32, 0, x_25);
+lean::cnstr_set(x_32, 1, x_30);
+return x_32;
+}
+else
+{
+obj* x_33; obj* x_34; obj* x_35; obj* x_36; 
+x_33 = lean::cnstr_get(x_29, 0);
+lean::inc(x_33);
+x_34 = lean::cnstr_get(x_29, 1);
+lean::inc(x_34);
+if (lean::is_exclusive(x_29)) {
+ lean::cnstr_release(x_29, 0);
+ lean::cnstr_release(x_29, 1);
+ x_35 = x_29;
+} else {
+ lean::dec_ref(x_29);
+ x_35 = lean::box(0);
+}
+if (lean::is_scalar(x_35)) {
+ x_36 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_36 = x_35;
+}
+lean::cnstr_set(x_36, 0, x_33);
+lean::cnstr_set(x_36, 1, x_34);
+return x_36;
+}
+}
+}
+else
+{
+uint8 x_37; 
+lean::dec(x_2);
+x_37 = !lean::is_exclusive(x_8);
+if (x_37 == 0)
+{
+return x_8;
+}
+else
+{
+obj* x_38; obj* x_39; obj* x_40; 
+x_38 = lean::cnstr_get(x_8, 0);
+x_39 = lean::cnstr_get(x_8, 1);
+lean::inc(x_39);
+lean::inc(x_38);
+lean::dec(x_8);
+x_40 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_40, 0, x_38);
+lean::cnstr_set(x_40, 1, x_39);
+return x_40;
+}
+}
+}
+}
+obj* l_Lean_Elab_elabPreTerm___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Lean_Elab_elabPreTerm(x_1, x_2, x_3);
+lean::dec(x_1);
+return x_4;
+}
+}
+obj* _init_l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__1() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::mk_string("elabPreTerm");
+return x_1;
+}
+}
+obj* _init_l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__2() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
+x_2 = l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+obj* _init_l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__3() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elab_elabPreTerm___boxed), 3, 0);
+return x_1;
+}
+}
+obj* l___regBuiltinTermElab_Lean_Elab_elabPreTerm(obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; obj* x_4; obj* x_5; 
+x_2 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
+x_3 = l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__2;
+x_4 = l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__3;
+x_5 = l_Lean_addBuiltinCommandElab(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
 obj* l_Lean_Elab_elabMixfix___rarg(obj* x_1) {
 _start:
 {
@@ -6794,7 +6993,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__2() {
 _start:
 {
 obj* x_1; obj* x_2; obj* x_3; 
-x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 x_2 = l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -6877,7 +7076,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabReserve___closed__2() {
 _start:
 {
 obj* x_1; obj* x_2; obj* x_3; 
-x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 x_2 = l___regBuiltinTermElab_Lean_Elab_elabReserve___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -6960,7 +7159,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabNotation___closed__2() {
 _start:
 {
 obj* x_1; obj* x_2; obj* x_3; 
-x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 x_2 = l___regBuiltinTermElab_Lean_Elab_elabNotation___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -6988,6 +7187,7 @@ return x_5;
 obj* initialize_init_lean_elaborator_alias(obj*);
 obj* initialize_init_lean_elaborator_basic(obj*);
 obj* initialize_init_lean_elaborator_resolvename(obj*);
+obj* initialize_init_lean_elaborator_preterm(obj*);
 static bool _G_initialized = false;
 obj* initialize_init_lean_elaborator_command(obj* w) {
 if (_G_initialized) return w;
@@ -6999,16 +7199,14 @@ w = initialize_init_lean_elaborator_basic(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_elaborator_resolvename(w);
 if (io_result_is_error(w)) return w;
+w = initialize_init_lean_elaborator_preterm(w);
+if (io_result_is_error(w)) return w;
 l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__1();
 lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__1);
 l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2();
 lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2);
 l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__3();
 lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__3);
-l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__4 = _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__4();
-lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__4);
-l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__5 = _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__5();
-lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__5);
 w = l___regBuiltinTermElab_Lean_Elab_elabNamespace(w);
 if (io_result_is_error(w)) return w;
 l___regBuiltinTermElab_Lean_Elab_elabSection___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_elabSection___closed__1();
@@ -7095,6 +7293,14 @@ l___regBuiltinTermElab_Lean_Elab_elabResolveName___closed__3 = _init_l___regBuil
 lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabResolveName___closed__3);
 w = l___regBuiltinTermElab_Lean_Elab_elabResolveName(w);
 if (io_result_is_error(w)) return w;
+l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__1();
+lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__1);
+l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__2();
+lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__2);
+l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__3();
+lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__3);
+w = l___regBuiltinTermElab_Lean_Elab_elabPreTerm(w);
+if (io_result_is_error(w)) return w;
 l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__1();
 lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__1);
 l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__2();
diff --git a/src/stage0/init/lean/elaborator/preterm.cpp b/src/stage0/init/lean/elaborator/preterm.cpp
index 34ce5ba0a4..1bf44395d7 100644
--- a/src/stage0/init/lean/elaborator/preterm.cpp
+++ b/src/stage0/init/lean/elaborator/preterm.cpp
@@ -14,21 +14,29 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-label"
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
+extern "C" obj* lean_expr_mk_mdata(obj*, obj*);
 obj* l_Lean_addBuiltinPreTermElab(obj*, obj*, obj*, obj*);
 obj* l_Lean_registerBuiltinPreTermElabAttr___closed__2;
 obj* l_Lean_registerBuiltinPreTermElabAttr___closed__3;
 obj* l_Lean_registerBuiltinPreTermElabAttr___closed__5;
 extern "C" uint8 lean_name_dec_eq(obj*, obj*);
+extern "C" obj* lean_expr_mk_sort(obj*);
+obj* l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1(obj*, obj*);
+obj* l_Lean_Elab_runIOUnsafe___rarg(obj*, obj*, obj*);
 obj* l_Array_mkArray(obj*, obj*, obj*);
 obj* l_Lean_builtinPreTermElabTable;
-extern obj* l_Lean_declareBuiltinTermElab___closed__2;
+obj* l_Lean_Elab_convertType___rarg(obj*);
 obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__4;
 extern obj* l_Lean_AttributeImpl_inhabited___closed__5;
 obj* l_HashMapImp_insert___at_Lean_addBuiltinPreTermElab___spec__3(obj*, obj*, obj*);
 extern obj* l_Lean_addBuiltinTermElab___closed__2;
 obj* l_Lean_mkBuiltinPreTermElabTable___closed__1;
+obj* l___regBuiltinTermElab_Lean_Elab_convertSort___closed__3;
 obj* l_Lean_registerAttribute(obj*, obj*);
 obj* l_Lean_registerBuiltinPreTermElabAttr___closed__7;
+obj* l_Lean_Elab_convertSort___boxed(obj*, obj*);
+obj* l___regBuiltinTermElab_Lean_Elab_convertType___closed__5;
+obj* l_Lean_Elab_convertType(obj*, obj*);
 obj* l_Array_uget(obj*, obj*, usize, obj*);
 obj* l_Lean_Name_toStringWithSep___main(obj*, obj*);
 extern obj* l_Lean_mkInitAttr___lambda__1___closed__1;
@@ -36,23 +44,44 @@ obj* l_Array_uset(obj*, obj*, usize, obj*, obj*);
 uint8 l_AssocList_contains___main___at_Lean_addBuiltinPreTermElab___spec__2(obj*, obj*);
 obj* l_IO_Prim_Ref_set(obj*, obj*, obj*, obj*);
 obj* l_Lean_registerBuiltinPreTermElabAttr___closed__4;
+obj* l_Lean_Elab_toPreTerm___closed__2;
+obj* l_Lean_declareBuiltinPreTermElab___closed__2;
+obj* l___regBuiltinTermElab_Lean_Elab_convertType___closed__1;
+obj* l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2(obj*, obj*);
+obj* l___private_init_lean_elaborator_preterm_1__dummy___closed__1;
+obj* l_IO_Prim_Ref_get___boxed(obj*, obj*, obj*);
+obj* l___regBuiltinTermElab_Lean_Elab_convertType___closed__3;
+obj* l___regBuiltinTermElab_Lean_Elab_convertSort___closed__2;
 obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__3;
+obj* l_Lean_declareBuiltinPreTermElab___closed__1;
 obj* l_mkHashMap___at_Lean_mkBuiltinPreTermElabTable___spec__1(obj*);
 extern obj* l_Lean_AttributeImpl_inhabited___closed__4;
 obj* l_Lean_registerTagAttribute___lambda__5___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l___private_init_lean_elaborator_preterm_1__dummy;
 obj* l_Lean_registerBuiltinPreTermElabAttr___closed__1;
+obj* l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1___boxed(obj*, obj*);
 obj* l_Lean_registerBuiltinPreTermElabAttr(obj*);
+extern "C" obj* lean_expr_mk_const(obj*, obj*);
+obj* l_Lean_Elab_convertSort(obj*, obj*);
 extern "C" usize lean_name_hash_usize(obj*);
+obj* l_Lean_Elab_toPreTerm___closed__1;
+extern obj* l_Lean_Parser_Term_prop___elambda__1___rarg___closed__3;
 namespace lean {
 obj* string_append(obj*, obj*);
 }
 obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l_Lean_KVMap_setName(obj*, obj*, obj*);
+extern obj* l_Lean_Parser_Term_sort___elambda__1___rarg___closed__2;
+extern obj* l_Lean_Parser_Term_type___elambda__1___rarg___closed__2;
 obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__1;
 namespace lean {
 uint8 nat_dec_lt(obj*, obj*);
 }
 obj* l_HashMapImp_contains___at_Lean_addBuiltinPreTermElab___spec__1___boxed(obj*, obj*);
+extern obj* l_Char_HasRepr___closed__1;
 extern obj* l_Lean_addBuiltinTermElab___closed__1;
+obj* l___regBuiltinTermElab_Lean_Elab_convertType___closed__4;
+obj* l___private_init_lean_elaborator_preterm_1__dummy___closed__2;
 obj* l_Array_fget(obj*, obj*, obj*);
 extern "C" obj* lean_name_mk_string(obj*, obj*);
 obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1(obj*, obj*, obj*, uint8, obj*);
@@ -61,41 +90,58 @@ obj* nat_add(obj*, obj*);
 }
 uint8 l_HashMapImp_contains___at_Lean_addBuiltinPreTermElab___spec__1(obj*, obj*);
 extern obj* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2;
+obj* l_Lean_Elab_convertSort___rarg(obj*);
 obj* l_Lean_addBuiltinPreTermElab___boxed(obj*, obj*, obj*, obj*);
+obj* l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2___boxed(obj*, obj*);
 obj* l_Lean_syntaxNodeKindOfAttrParam(obj*, obj*, obj*, obj*);
 obj* l_Lean_registerBuiltinPreTermElabAttr___closed__6;
 obj* l_IO_Prim_mkRef(obj*, obj*, obj*);
 obj* l_HashMapImp_expand___at_Lean_addBuiltinPreTermElab___spec__4(obj*, obj*);
+obj* l___regBuiltinTermElab_Lean_Elab_convertType(obj*);
+extern obj* l_Lean_Level_one___closed__1;
 obj* l_HashMapImp_moveEntries___main___at_Lean_addBuiltinPreTermElab___spec__5(obj*, obj*, obj*);
+obj* l_Lean_Elab_toPreTerm___closed__3;
 extern obj* l_System_FilePath_dirName___closed__1;
 obj* l_IO_Prim_Ref_get(obj*, obj*, obj*);
+obj* l_Lean_Expr_mkAnnotation___closed__1;
 namespace lean {
 usize usize_modn(usize, obj*);
 }
 obj* l_Lean_ConstantInfo_type(obj*);
+obj* l_Lean_Expr_mkAnnotation(obj*, obj*);
 obj* l_Lean_mkBuiltinPreTermElabTable(obj*);
 namespace lean {
 obj* environment_find_core(obj*, obj*);
 }
+obj* l___regBuiltinTermElab_Lean_Elab_convertSort___closed__1;
+obj* l_Lean_Elab_toPreTerm(obj*, obj*, obj*);
 obj* l_AssocList_mfoldl___main___at_Lean_addBuiltinPreTermElab___spec__6(obj*, obj*);
 obj* l_Array_size(obj*, obj*);
 obj* l_Array_fset(obj*, obj*, obj*, obj*);
+obj* l_Lean_Elab_convertType___boxed(obj*, obj*);
 obj* l_mkHashMapImp___rarg(obj*);
 obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__2;
 extern obj* l_Lean_nameToExprAux___main___closed__4;
 namespace lean {
 uint8 nat_dec_le(obj*, obj*);
 }
+obj* l___regBuiltinTermElab_Lean_Elab_convertSort(obj*);
 obj* l_AssocList_replace___main___at_Lean_addBuiltinPreTermElab___spec__7(obj*, obj*, obj*);
 obj* l_Lean_declareBuiltinElab(obj*, obj*, obj*, obj*, obj*);
 namespace lean {
 obj* nat_mul(obj*, obj*);
 }
 obj* l_AssocList_contains___main___at_Lean_addBuiltinPreTermElab___spec__2___boxed(obj*, obj*);
+obj* l_Lean_Expr_mkAnnotation___closed__2;
+obj* l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
 obj* l_IO_Prim_Ref_reset(obj*, obj*, obj*);
+obj* l_Lean_Elab_convertType___rarg___closed__1;
+extern obj* l_Lean_exprIsInhabited___closed__1;
 obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__5;
 obj* l_Lean_declareBuiltinPreTermElab(obj*, obj*, obj*, obj*);
+obj* l_Lean_logErrorAndThrow___rarg(obj*, obj*, obj*, obj*);
 obj* l_Lean_registerTagAttribute___lambda__6___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l_Lean_Elab_toPreTerm___closed__4;
 obj* l_mkHashMap___at_Lean_mkBuiltinPreTermElabTable___spec__1(obj* x_1) {
 _start:
 {
@@ -857,11 +903,29 @@ lean::dec(x_2);
 return x_5;
 }
 }
+obj* _init_l_Lean_declareBuiltinPreTermElab___closed__1() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::mk_string("addBuiltinPreTermElab");
+return x_1;
+}
+}
+obj* _init_l_Lean_declareBuiltinPreTermElab___closed__2() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_nameToExprAux___main___closed__4;
+x_2 = l_Lean_declareBuiltinPreTermElab___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
 obj* l_Lean_declareBuiltinPreTermElab(obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
 obj* x_5; obj* x_6; 
-x_5 = l_Lean_declareBuiltinTermElab___closed__2;
+x_5 = l_Lean_declareBuiltinPreTermElab___closed__2;
 x_6 = l_Lean_declareBuiltinElab(x_1, x_5, x_2, x_3, x_4);
 return x_6;
 }
@@ -1325,6 +1389,606 @@ lean::dec(x_3);
 return x_7;
 }
 }
+obj* _init_l_Lean_Expr_mkAnnotation___closed__1() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::mk_string("annotation");
+return x_1;
+}
+}
+obj* _init_l_Lean_Expr_mkAnnotation___closed__2() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = lean::box(0);
+x_2 = l_Lean_Expr_mkAnnotation___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+obj* l_Lean_Expr_mkAnnotation(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; obj* x_4; obj* x_5; obj* x_6; 
+x_3 = lean::box(0);
+x_4 = l_Lean_Expr_mkAnnotation___closed__2;
+x_5 = l_Lean_KVMap_setName(x_3, x_4, x_1);
+x_6 = lean_expr_mk_mdata(x_5, x_2);
+return x_6;
+}
+}
+obj* _init_l___private_init_lean_elaborator_preterm_1__dummy___closed__1() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = lean::box(0);
+x_2 = l_Lean_Parser_Term_prop___elambda__1___rarg___closed__3;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+obj* _init_l___private_init_lean_elaborator_preterm_1__dummy___closed__2() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = lean::box(0);
+x_2 = l___private_init_lean_elaborator_preterm_1__dummy___closed__1;
+x_3 = lean_expr_mk_const(x_2, x_1);
+return x_3;
+}
+}
+obj* _init_l___private_init_lean_elaborator_preterm_1__dummy() {
+_start:
+{
+obj* x_1; 
+x_1 = l___private_init_lean_elaborator_preterm_1__dummy___closed__2;
+return x_1;
+}
+}
+obj* l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2(obj* x_1, obj* x_2) {
+_start:
+{
+if (lean::obj_tag(x_2) == 0)
+{
+obj* x_3; 
+x_3 = lean::box(0);
+return x_3;
+}
+else
+{
+obj* x_4; obj* x_5; obj* x_6; uint8 x_7; 
+x_4 = lean::cnstr_get(x_2, 0);
+x_5 = lean::cnstr_get(x_2, 1);
+x_6 = lean::cnstr_get(x_2, 2);
+x_7 = lean_name_dec_eq(x_4, x_1);
+if (x_7 == 0)
+{
+x_2 = x_6;
+goto _start;
+}
+else
+{
+obj* x_9; 
+lean::inc(x_5);
+x_9 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_9, 0, x_5);
+return x_9;
+}
+}
+}
+}
+obj* l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; obj* x_4; usize x_5; usize x_6; obj* x_7; usize x_8; obj* x_9; obj* x_10; 
+x_3 = lean::cnstr_get(x_1, 1);
+x_4 = lean::array_get_size(x_3);
+x_5 = lean_name_hash_usize(x_2);
+x_6 = lean::usize_modn(x_5, x_4);
+lean::dec(x_4);
+x_7 = lean::box_size_t(x_6);
+x_8 = lean::unbox_size_t(x_7);
+lean::dec(x_7);
+x_9 = lean::array_uget(x_3, x_8);
+x_10 = l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2(x_2, x_9);
+lean::dec(x_9);
+return x_10;
+}
+}
+obj* _init_l_Lean_Elab_toPreTerm___closed__1() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::mk_string("`toPreTerm` failed, unexpected syntax");
+return x_1;
+}
+}
+obj* _init_l_Lean_Elab_toPreTerm___closed__2() {
+_start:
+{
+obj* x_1; obj* x_2; 
+x_1 = l_Lean_Elab_toPreTerm___closed__1;
+x_2 = lean::alloc_cnstr(3, 1, 0);
+lean::cnstr_set(x_2, 0, x_1);
+return x_2;
+}
+}
+obj* _init_l_Lean_Elab_toPreTerm___closed__3() {
+_start:
+{
+obj* x_1; obj* x_2; 
+x_1 = l_Lean_builtinPreTermElabTable;
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_IO_Prim_Ref_get___boxed), 3, 2);
+lean::closure_set(x_2, 0, lean::box(0));
+lean::closure_set(x_2, 1, x_1);
+return x_2;
+}
+}
+obj* _init_l_Lean_Elab_toPreTerm___closed__4() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::mk_string("`toPreTerm` failed, no support for syntax '");
+return x_1;
+}
+}
+obj* l_Lean_Elab_toPreTerm(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+if (lean::obj_tag(x_1) == 1)
+{
+obj* x_4; uint8 x_5; 
+x_4 = lean::cnstr_get(x_1, 0);
+lean::inc(x_4);
+x_5 = !lean::is_exclusive(x_3);
+if (x_5 == 0)
+{
+obj* x_6; obj* x_7; obj* x_8; obj* x_9; 
+x_6 = lean::cnstr_get(x_3, 0);
+lean::dec(x_6);
+x_7 = lean::box(0);
+lean::cnstr_set(x_3, 0, x_7);
+x_8 = l_Lean_Elab_toPreTerm___closed__3;
+x_9 = l_Lean_Elab_runIOUnsafe___rarg(x_8, x_2, x_3);
+if (lean::obj_tag(x_9) == 0)
+{
+uint8 x_10; 
+x_10 = !lean::is_exclusive(x_9);
+if (x_10 == 0)
+{
+obj* x_11; obj* x_12; 
+x_11 = lean::cnstr_get(x_9, 0);
+lean::cnstr_set(x_9, 0, x_7);
+x_12 = l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1(x_11, x_4);
+lean::dec(x_11);
+if (lean::obj_tag(x_12) == 0)
+{
+obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; 
+x_13 = l_System_FilePath_dirName___closed__1;
+x_14 = l_Lean_Name_toStringWithSep___main(x_13, x_4);
+x_15 = l_Lean_Elab_toPreTerm___closed__4;
+x_16 = lean::string_append(x_15, x_14);
+lean::dec(x_14);
+x_17 = l_Char_HasRepr___closed__1;
+x_18 = lean::string_append(x_16, x_17);
+x_19 = l_Lean_logErrorAndThrow___rarg(x_1, x_18, x_2, x_9);
+lean::dec(x_2);
+lean::dec(x_1);
+return x_19;
+}
+else
+{
+obj* x_20; obj* x_21; 
+lean::dec(x_4);
+x_20 = lean::cnstr_get(x_12, 0);
+lean::inc(x_20);
+lean::dec(x_12);
+x_21 = lean::apply_3(x_20, x_1, x_2, x_9);
+return x_21;
+}
+}
+else
+{
+obj* x_22; obj* x_23; obj* x_24; obj* x_25; 
+x_22 = lean::cnstr_get(x_9, 0);
+x_23 = lean::cnstr_get(x_9, 1);
+lean::inc(x_23);
+lean::inc(x_22);
+lean::dec(x_9);
+x_24 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_24, 0, x_7);
+lean::cnstr_set(x_24, 1, x_23);
+x_25 = l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1(x_22, x_4);
+lean::dec(x_22);
+if (lean::obj_tag(x_25) == 0)
+{
+obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_31; obj* x_32; 
+x_26 = l_System_FilePath_dirName___closed__1;
+x_27 = l_Lean_Name_toStringWithSep___main(x_26, x_4);
+x_28 = l_Lean_Elab_toPreTerm___closed__4;
+x_29 = lean::string_append(x_28, x_27);
+lean::dec(x_27);
+x_30 = l_Char_HasRepr___closed__1;
+x_31 = lean::string_append(x_29, x_30);
+x_32 = l_Lean_logErrorAndThrow___rarg(x_1, x_31, x_2, x_24);
+lean::dec(x_2);
+lean::dec(x_1);
+return x_32;
+}
+else
+{
+obj* x_33; obj* x_34; 
+lean::dec(x_4);
+x_33 = lean::cnstr_get(x_25, 0);
+lean::inc(x_33);
+lean::dec(x_25);
+x_34 = lean::apply_3(x_33, x_1, x_2, x_24);
+return x_34;
+}
+}
+}
+else
+{
+uint8 x_35; 
+lean::dec(x_4);
+lean::dec(x_2);
+lean::dec(x_1);
+x_35 = !lean::is_exclusive(x_9);
+if (x_35 == 0)
+{
+return x_9;
+}
+else
+{
+obj* x_36; obj* x_37; obj* x_38; 
+x_36 = lean::cnstr_get(x_9, 0);
+x_37 = lean::cnstr_get(x_9, 1);
+lean::inc(x_37);
+lean::inc(x_36);
+lean::dec(x_9);
+x_38 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_38, 0, x_36);
+lean::cnstr_set(x_38, 1, x_37);
+return x_38;
+}
+}
+}
+else
+{
+obj* x_39; obj* x_40; obj* x_41; obj* x_42; obj* x_43; 
+x_39 = lean::cnstr_get(x_3, 1);
+lean::inc(x_39);
+lean::dec(x_3);
+x_40 = lean::box(0);
+x_41 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_41, 0, x_40);
+lean::cnstr_set(x_41, 1, x_39);
+x_42 = l_Lean_Elab_toPreTerm___closed__3;
+x_43 = l_Lean_Elab_runIOUnsafe___rarg(x_42, x_2, x_41);
+if (lean::obj_tag(x_43) == 0)
+{
+obj* x_44; obj* x_45; obj* x_46; obj* x_47; obj* x_48; 
+x_44 = lean::cnstr_get(x_43, 0);
+lean::inc(x_44);
+x_45 = lean::cnstr_get(x_43, 1);
+lean::inc(x_45);
+if (lean::is_exclusive(x_43)) {
+ lean::cnstr_release(x_43, 0);
+ lean::cnstr_release(x_43, 1);
+ x_46 = x_43;
+} else {
+ lean::dec_ref(x_43);
+ x_46 = lean::box(0);
+}
+if (lean::is_scalar(x_46)) {
+ x_47 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_47 = x_46;
+}
+lean::cnstr_set(x_47, 0, x_40);
+lean::cnstr_set(x_47, 1, x_45);
+x_48 = l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1(x_44, x_4);
+lean::dec(x_44);
+if (lean::obj_tag(x_48) == 0)
+{
+obj* x_49; obj* x_50; obj* x_51; obj* x_52; obj* x_53; obj* x_54; obj* x_55; 
+x_49 = l_System_FilePath_dirName___closed__1;
+x_50 = l_Lean_Name_toStringWithSep___main(x_49, x_4);
+x_51 = l_Lean_Elab_toPreTerm___closed__4;
+x_52 = lean::string_append(x_51, x_50);
+lean::dec(x_50);
+x_53 = l_Char_HasRepr___closed__1;
+x_54 = lean::string_append(x_52, x_53);
+x_55 = l_Lean_logErrorAndThrow___rarg(x_1, x_54, x_2, x_47);
+lean::dec(x_2);
+lean::dec(x_1);
+return x_55;
+}
+else
+{
+obj* x_56; obj* x_57; 
+lean::dec(x_4);
+x_56 = lean::cnstr_get(x_48, 0);
+lean::inc(x_56);
+lean::dec(x_48);
+x_57 = lean::apply_3(x_56, x_1, x_2, x_47);
+return x_57;
+}
+}
+else
+{
+obj* x_58; obj* x_59; obj* x_60; obj* x_61; 
+lean::dec(x_4);
+lean::dec(x_2);
+lean::dec(x_1);
+x_58 = lean::cnstr_get(x_43, 0);
+lean::inc(x_58);
+x_59 = lean::cnstr_get(x_43, 1);
+lean::inc(x_59);
+if (lean::is_exclusive(x_43)) {
+ lean::cnstr_release(x_43, 0);
+ lean::cnstr_release(x_43, 1);
+ x_60 = x_43;
+} else {
+ lean::dec_ref(x_43);
+ x_60 = lean::box(0);
+}
+if (lean::is_scalar(x_60)) {
+ x_61 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_61 = x_60;
+}
+lean::cnstr_set(x_61, 0, x_58);
+lean::cnstr_set(x_61, 1, x_59);
+return x_61;
+}
+}
+}
+else
+{
+uint8 x_62; 
+lean::dec(x_2);
+lean::dec(x_1);
+x_62 = !lean::is_exclusive(x_3);
+if (x_62 == 0)
+{
+obj* x_63; obj* x_64; 
+x_63 = lean::cnstr_get(x_3, 0);
+lean::dec(x_63);
+x_64 = l_Lean_Elab_toPreTerm___closed__2;
+lean::cnstr_set_tag(x_3, 1);
+lean::cnstr_set(x_3, 0, x_64);
+return x_3;
+}
+else
+{
+obj* x_65; obj* x_66; obj* x_67; 
+x_65 = lean::cnstr_get(x_3, 1);
+lean::inc(x_65);
+lean::dec(x_3);
+x_66 = l_Lean_Elab_toPreTerm___closed__2;
+x_67 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_67, 0, x_66);
+lean::cnstr_set(x_67, 1, x_65);
+return x_67;
+}
+}
+}
+}
+obj* l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2___boxed(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2(x_1, x_2);
+lean::dec(x_2);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1___boxed(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1(x_1, x_2);
+lean::dec(x_2);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* _init_l_Lean_Elab_convertType___rarg___closed__1() {
+_start:
+{
+obj* x_1; obj* x_2; 
+x_1 = l_Lean_Level_one___closed__1;
+x_2 = lean_expr_mk_sort(x_1);
+return x_2;
+}
+}
+obj* l_Lean_Elab_convertType___rarg(obj* x_1) {
+_start:
+{
+uint8 x_2; 
+x_2 = !lean::is_exclusive(x_1);
+if (x_2 == 0)
+{
+obj* x_3; obj* x_4; 
+x_3 = lean::cnstr_get(x_1, 0);
+lean::dec(x_3);
+x_4 = l_Lean_Elab_convertType___rarg___closed__1;
+lean::cnstr_set(x_1, 0, x_4);
+return x_1;
+}
+else
+{
+obj* x_5; obj* x_6; obj* x_7; 
+x_5 = lean::cnstr_get(x_1, 1);
+lean::inc(x_5);
+lean::dec(x_1);
+x_6 = l_Lean_Elab_convertType___rarg___closed__1;
+x_7 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_7, 0, x_6);
+lean::cnstr_set(x_7, 1, x_5);
+return x_7;
+}
+}
+}
+obj* l_Lean_Elab_convertType(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elab_convertType___rarg), 1, 0);
+return x_3;
+}
+}
+obj* l_Lean_Elab_convertType___boxed(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Lean_Elab_convertType(x_1, x_2);
+lean::dec(x_2);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__1() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::mk_string("Elab");
+return x_1;
+}
+}
+obj* _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__2() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_nameToExprAux___main___closed__4;
+x_2 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+obj* _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__3() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::mk_string("convertType");
+return x_1;
+}
+}
+obj* _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__4() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
+x_2 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__3;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+obj* _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__5() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elab_convertType___boxed), 2, 0);
+return x_1;
+}
+}
+obj* l___regBuiltinTermElab_Lean_Elab_convertType(obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; obj* x_4; obj* x_5; 
+x_2 = l_Lean_Parser_Term_type___elambda__1___rarg___closed__2;
+x_3 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__4;
+x_4 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__5;
+x_5 = l_Lean_addBuiltinPreTermElab(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
+obj* l_Lean_Elab_convertSort___rarg(obj* x_1) {
+_start:
+{
+uint8 x_2; 
+x_2 = !lean::is_exclusive(x_1);
+if (x_2 == 0)
+{
+obj* x_3; obj* x_4; 
+x_3 = lean::cnstr_get(x_1, 0);
+lean::dec(x_3);
+x_4 = l_Lean_exprIsInhabited___closed__1;
+lean::cnstr_set(x_1, 0, x_4);
+return x_1;
+}
+else
+{
+obj* x_5; obj* x_6; obj* x_7; 
+x_5 = lean::cnstr_get(x_1, 1);
+lean::inc(x_5);
+lean::dec(x_1);
+x_6 = l_Lean_exprIsInhabited___closed__1;
+x_7 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_7, 0, x_6);
+lean::cnstr_set(x_7, 1, x_5);
+return x_7;
+}
+}
+}
+obj* l_Lean_Elab_convertSort(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elab_convertSort___rarg), 1, 0);
+return x_3;
+}
+}
+obj* l_Lean_Elab_convertSort___boxed(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Lean_Elab_convertSort(x_1, x_2);
+lean::dec(x_2);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* _init_l___regBuiltinTermElab_Lean_Elab_convertSort___closed__1() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::mk_string("convertSort");
+return x_1;
+}
+}
+obj* _init_l___regBuiltinTermElab_Lean_Elab_convertSort___closed__2() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
+x_2 = l___regBuiltinTermElab_Lean_Elab_convertSort___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+obj* _init_l___regBuiltinTermElab_Lean_Elab_convertSort___closed__3() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elab_convertSort___boxed), 2, 0);
+return x_1;
+}
+}
+obj* l___regBuiltinTermElab_Lean_Elab_convertSort(obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; obj* x_4; obj* x_5; 
+x_2 = l_Lean_Parser_Term_sort___elambda__1___rarg___closed__2;
+x_3 = l___regBuiltinTermElab_Lean_Elab_convertSort___closed__2;
+x_4 = l___regBuiltinTermElab_Lean_Elab_convertSort___closed__3;
+x_5 = l_Lean_addBuiltinPreTermElab(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
 obj* initialize_init_lean_elaborator_basic(obj*);
 static bool _G_initialized = false;
 obj* initialize_init_lean_elaborator_preterm(obj* w) {
@@ -1339,6 +2003,10 @@ w = l_Lean_mkBuiltinPreTermElabTable(w);
 if (io_result_is_error(w)) return w;
 l_Lean_builtinPreTermElabTable = io_result_get_value(w);
 lean::mark_persistent(l_Lean_builtinPreTermElabTable);
+l_Lean_declareBuiltinPreTermElab___closed__1 = _init_l_Lean_declareBuiltinPreTermElab___closed__1();
+lean::mark_persistent(l_Lean_declareBuiltinPreTermElab___closed__1);
+l_Lean_declareBuiltinPreTermElab___closed__2 = _init_l_Lean_declareBuiltinPreTermElab___closed__2();
+lean::mark_persistent(l_Lean_declareBuiltinPreTermElab___closed__2);
 l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__1 = _init_l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__1();
 lean::mark_persistent(l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__1);
 l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__2 = _init_l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__2();
@@ -1365,5 +2033,45 @@ l_Lean_registerBuiltinPreTermElabAttr___closed__7 = _init_l_Lean_registerBuiltin
 lean::mark_persistent(l_Lean_registerBuiltinPreTermElabAttr___closed__7);
 w = l_Lean_registerBuiltinPreTermElabAttr(w);
 if (io_result_is_error(w)) return w;
+l_Lean_Expr_mkAnnotation___closed__1 = _init_l_Lean_Expr_mkAnnotation___closed__1();
+lean::mark_persistent(l_Lean_Expr_mkAnnotation___closed__1);
+l_Lean_Expr_mkAnnotation___closed__2 = _init_l_Lean_Expr_mkAnnotation___closed__2();
+lean::mark_persistent(l_Lean_Expr_mkAnnotation___closed__2);
+l___private_init_lean_elaborator_preterm_1__dummy___closed__1 = _init_l___private_init_lean_elaborator_preterm_1__dummy___closed__1();
+lean::mark_persistent(l___private_init_lean_elaborator_preterm_1__dummy___closed__1);
+l___private_init_lean_elaborator_preterm_1__dummy___closed__2 = _init_l___private_init_lean_elaborator_preterm_1__dummy___closed__2();
+lean::mark_persistent(l___private_init_lean_elaborator_preterm_1__dummy___closed__2);
+l___private_init_lean_elaborator_preterm_1__dummy = _init_l___private_init_lean_elaborator_preterm_1__dummy();
+lean::mark_persistent(l___private_init_lean_elaborator_preterm_1__dummy);
+l_Lean_Elab_toPreTerm___closed__1 = _init_l_Lean_Elab_toPreTerm___closed__1();
+lean::mark_persistent(l_Lean_Elab_toPreTerm___closed__1);
+l_Lean_Elab_toPreTerm___closed__2 = _init_l_Lean_Elab_toPreTerm___closed__2();
+lean::mark_persistent(l_Lean_Elab_toPreTerm___closed__2);
+l_Lean_Elab_toPreTerm___closed__3 = _init_l_Lean_Elab_toPreTerm___closed__3();
+lean::mark_persistent(l_Lean_Elab_toPreTerm___closed__3);
+l_Lean_Elab_toPreTerm___closed__4 = _init_l_Lean_Elab_toPreTerm___closed__4();
+lean::mark_persistent(l_Lean_Elab_toPreTerm___closed__4);
+l_Lean_Elab_convertType___rarg___closed__1 = _init_l_Lean_Elab_convertType___rarg___closed__1();
+lean::mark_persistent(l_Lean_Elab_convertType___rarg___closed__1);
+l___regBuiltinTermElab_Lean_Elab_convertType___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__1();
+lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertType___closed__1);
+l___regBuiltinTermElab_Lean_Elab_convertType___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__2();
+lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertType___closed__2);
+l___regBuiltinTermElab_Lean_Elab_convertType___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__3();
+lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertType___closed__3);
+l___regBuiltinTermElab_Lean_Elab_convertType___closed__4 = _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__4();
+lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertType___closed__4);
+l___regBuiltinTermElab_Lean_Elab_convertType___closed__5 = _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__5();
+lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertType___closed__5);
+w = l___regBuiltinTermElab_Lean_Elab_convertType(w);
+if (io_result_is_error(w)) return w;
+l___regBuiltinTermElab_Lean_Elab_convertSort___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_convertSort___closed__1();
+lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertSort___closed__1);
+l___regBuiltinTermElab_Lean_Elab_convertSort___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_convertSort___closed__2();
+lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertSort___closed__2);
+l___regBuiltinTermElab_Lean_Elab_convertSort___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_convertSort___closed__3();
+lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertSort___closed__3);
+w = l___regBuiltinTermElab_Lean_Elab_convertSort(w);
+if (io_result_is_error(w)) return w;
 return w;
 }
diff --git a/src/stage0/init/lean/parser/command.cpp b/src/stage0/init/lean/parser/command.cpp
index 27ae223fc2..5b3500c0fc 100644
--- a/src/stage0/init/lean/parser/command.cpp
+++ b/src/stage0/init/lean/parser/command.cpp
@@ -38,6 +38,7 @@ obj* l_Lean_Parser_Command_reserve___elambda__1___closed__5;
 obj* l_Lean_Parser_Command_declId___closed__7;
 obj* l_Lean_Parser_Command_unsafe___elambda__1___rarg___closed__2;
 obj* l_Lean_Parser_Command_private___elambda__1___rarg___closed__7;
+obj* l___regBuiltinParser_Lean_Parser_Command_preterm(obj*);
 obj* l_Lean_Parser_Command_export;
 obj* l_Lean_Parser_Command_docComment___closed__2;
 obj* l_Lean_Parser_Command_openRenaming___closed__2;
@@ -129,6 +130,7 @@ obj* l___private_init_lean_parser_parser_2__sepByFnAux___main___at_Lean_Parser_C
 obj* l_Lean_Parser_Command_attributes___elambda__1___closed__1;
 obj* l_Lean_Parser_Command_set__option___closed__6;
 obj* l_Lean_Parser_Command_open___elambda__1___closed__3;
+obj* l_Lean_Parser_Command_preterm___closed__5;
 obj* l_Lean_Parser_Command_commentBody___elambda__1___boxed(obj*, obj*, obj*);
 obj* l_Lean_Parser_regBuiltinCommandParserAttr___closed__1;
 obj* l_Lean_Parser_Command_universe___elambda__1___rarg___closed__5;
@@ -205,6 +207,7 @@ obj* l_Lean_Parser_Command_infix___elambda__1___rarg___closed__2;
 obj* l_Lean_Parser_Command_structImplicitBinder___elambda__1___closed__2;
 obj* l_Lean_Parser_Command_end___closed__5;
 obj* l_Lean_Parser_Command_openSimple___elambda__1(obj*, obj*, obj*);
+obj* l_Lean_Parser_Command_preterm___closed__3;
 extern obj* l_Lean_Parser_Term_typeAscription___elambda__1___rarg___closed__4;
 obj* l_Lean_Parser_Command_strictInferMod___closed__1;
 obj* l_Lean_Parser_Command_resolve__name___elambda__1___rarg___closed__6;
@@ -221,6 +224,7 @@ obj* l_Lean_Parser_Command_open___closed__8;
 obj* l_Lean_Parser_Command_structCtor___elambda__1___rarg(obj*, obj*);
 obj* l_Lean_Parser_Command_commentBody;
 obj* l_Lean_Parser_Command_docComment___elambda__1___closed__2;
+obj* l_Lean_Parser_Command_preterm___elambda__1___boxed(obj*);
 obj* l_Lean_Parser_Command_unsafe___elambda__1(obj*);
 obj* l_Lean_Parser_Command_declId___elambda__1(obj*, obj*, obj*);
 obj* l_Lean_Parser_Command_abbrev___elambda__1___closed__4;
@@ -286,14 +290,17 @@ obj* l_Lean_Parser_Command_structExplicitBinder___closed__10;
 obj* l_Lean_Parser_Command_infix___closed__1;
 obj* l_Lean_Parser_Command_classTk___elambda__1___rarg___closed__1;
 obj* l_Lean_Parser_Command_declValSimple___elambda__1(obj*);
+obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__1;
 obj* l_Lean_Parser_Command_declValSimple;
 obj* l_Lean_Parser_Command_strictInferMod;
 obj* l_Lean_Parser_Command_namespace;
+obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__5;
 obj* l_Lean_Parser_Command_structImplicitBinder___closed__4;
 obj* l_Lean_Parser_Command_prefix___elambda__1___rarg(obj*, obj*);
 obj* l_Lean_Parser_Command_introRule___closed__6;
 obj* l_Lean_Parser_Command_constant___closed__5;
 obj* l_Lean_Parser_Command_postfix___elambda__1___rarg___closed__3;
+obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
 obj* l_Lean_Parser_Command_notation___closed__3;
 obj* l_Lean_Parser_Command_commentBody___closed__2;
 obj* l_Lean_Parser_Command_universes___closed__4;
@@ -457,12 +464,14 @@ obj* l_Lean_Parser_Command_infix___closed__3;
 obj* l_Lean_Parser_Command_exit___elambda__1___rarg___closed__1;
 obj* l_Lean_Parser_Command_attribute___elambda__1___closed__1;
 obj* l_Lean_Parser_Term_binderDefault___elambda__1___rarg(obj*, obj*);
+obj* l_Lean_Parser_Command_preterm___closed__2;
 obj* l_Lean_Parser_Command_visibility___elambda__1(obj*);
 obj* l_Lean_Parser_Command_openHiding___closed__6;
 obj* l_Lean_Parser_Command_docComment;
 obj* l_Lean_Parser_Command_openHiding___elambda__1___closed__2;
 obj* l_Lean_Parser_Command_example___elambda__1___closed__4;
 obj* l_Lean_Parser_Command_protected___closed__3;
+obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6;
 obj* l_Lean_Parser_Command_partial___closed__4;
 obj* l_Lean_Parser_ParserState_mkNode(obj*, obj*, obj*);
 obj* l_Lean_Parser_Command_mixfixKind___elambda__1___boxed(obj*);
@@ -489,6 +498,7 @@ obj* l_Lean_Parser_Command_attrInstance___closed__3;
 obj* l_Lean_Parser_Command_openHiding___closed__4;
 obj* l_Lean_Parser_Command_unsafe___closed__1;
 obj* l_Lean_Parser_Command_identPrec___closed__4;
+obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4;
 obj* l_Lean_Parser_Command_inductive___closed__3;
 obj* l_Lean_Parser_Command_set__option___elambda__1___rarg___closed__13;
 obj* l_Lean_Parser_Command_declaration___closed__12;
@@ -525,6 +535,7 @@ obj* l_Lean_Parser_Command_attrInstance;
 obj* l_Lean_Parser_Command_theorem___elambda__1___closed__6;
 obj* l_Lean_Parser_Command_attributes___elambda__1___closed__3;
 obj* l_Lean_Parser_Command_openOnly___elambda__1___closed__1;
+obj* l_Lean_Parser_Command_preterm;
 obj* l_Lean_Parser_Command_resolve__name___elambda__1___rarg___closed__4;
 obj* l_Lean_Parser_Command_export___closed__1;
 obj* l_Lean_Parser_Command_exit___elambda__1___rarg___closed__6;
@@ -826,6 +837,7 @@ obj* l_Lean_Parser_Command_namespace___closed__3;
 obj* l_Lean_Parser_Command_resolve__name___closed__2;
 obj* l_Lean_Parser_manyAux___main___at_Lean_Parser_Command_notation___elambda__1___spec__1___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_Command_partial___elambda__1___boxed(obj*);
+obj* l_Lean_Parser_Command_preterm___elambda__1(obj*);
 obj* l_Lean_Parser_Command_example___elambda__1(obj*, obj*, obj*);
 obj* l_Lean_Parser_Command_universe___closed__5;
 obj* l_Lean_Parser_Command_structureTk___closed__4;
@@ -840,6 +852,7 @@ obj* l_Lean_Parser_identFn___rarg(obj*, obj*);
 obj* l_Lean_Parser_Command_maxPrec___elambda__1___boxed(obj*);
 obj* l_Lean_Parser_Command_infixr___elambda__1___boxed(obj*);
 obj* l_Lean_Parser_Command_structExplicitBinder___closed__8;
+obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__3;
 obj* l_Lean_Parser_manyAux___main___at_Lean_Parser_Command_declValEqns___spec__2(obj*, uint8, obj*, obj*, obj*);
 obj* l_String_trim(obj*);
 obj* l_Lean_Parser_Command_universes___closed__3;
@@ -868,6 +881,7 @@ obj* l_Lean_Parser_Command_constant___closed__7;
 obj* l_Lean_Parser_Command_infixl___elambda__1___rarg___closed__2;
 obj* l_Lean_Parser_Command_quotedSymbolPrec___closed__3;
 obj* l_Lean_Parser_Command_strictInferMod___elambda__1___rarg(obj*, obj*);
+obj* l_Lean_Parser_Command_preterm___closed__1;
 obj* l_Lean_Parser_Command_declVal___elambda__1___boxed(obj*, obj*, obj*);
 obj* l_Lean_Parser_Command_openRenaming___elambda__1___closed__6;
 obj* l_Lean_Parser_Command_attribute___closed__9;
@@ -906,6 +920,7 @@ obj* l_Lean_Parser_Command_structureTk___elambda__1___boxed(obj*);
 obj* l_Lean_Parser_Command_protected___elambda__1___rarg___closed__7;
 obj* l_Lean_Parser_Command_universes;
 obj* l_Lean_Parser_Command_declModifiers___closed__6;
+obj* l_Lean_Parser_Command_preterm___closed__4;
 obj* l_Lean_Parser_Command_set__option___elambda__1___rarg(obj*, obj*);
 obj* l_Lean_Parser_Command_openSimple___closed__2;
 obj* l_Lean_Parser_Command_classInductive___elambda__1___closed__6;
@@ -963,6 +978,7 @@ obj* l_Lean_Parser_Command_declaration;
 obj* l_Lean_Parser_Command_private___elambda__1___rarg___closed__5;
 obj* l_Lean_Parser_Command_section___elambda__1___rarg___closed__2;
 obj* l_Lean_Parser_Command_unsafe___elambda__1___rarg___closed__3;
+obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7;
 obj* l_Lean_Parser_Command_structure___closed__5;
 obj* l_Lean_Parser_Command_openHiding___elambda__1___closed__4;
 obj* l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__1;
@@ -1045,6 +1061,7 @@ obj* l_Lean_Parser_Command_variable___elambda__1___closed__3;
 obj* l___regBuiltinParser_Lean_Parser_Command_end(obj*);
 obj* l_Lean_Parser_Command_declId___closed__3;
 obj* l_Lean_Parser_Command_noncomputable___elambda__1___rarg___closed__7;
+obj* l_Lean_Parser_Command_preterm___elambda__1___rarg(obj*, obj*);
 obj* l_Lean_Parser_Command_structInstBinder___closed__4;
 obj* l_Lean_Parser_Command_attribute___closed__5;
 obj* l_Lean_Parser_Command_openRenamingItem___elambda__1(obj*);
@@ -15909,6 +15926,250 @@ x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
+obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__1() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::mk_string("preterm");
+return x_1;
+}
+}
+obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Command_docComment___elambda__1___closed__2;
+x_2 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__3() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::mk_string("#preterm ");
+return x_1;
+}
+}
+obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4() {
+_start:
+{
+obj* x_1; obj* x_2; 
+x_1 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__3;
+x_2 = l_String_trim(x_1);
+return x_2;
+}
+}
+obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__5() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Char_HasRepr___closed__1;
+x_2 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4;
+x_3 = lean::string_append(x_1, x_2);
+return x_3;
+}
+}
+obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__5;
+x_2 = l_Char_HasRepr___closed__1;
+x_3 = lean::string_append(x_1, x_2);
+return x_3;
+}
+}
+obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = lean::box(0);
+x_2 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6;
+x_3 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_3, 0, x_2);
+lean::cnstr_set(x_3, 1, x_1);
+return x_3;
+}
+}
+obj* l_Lean_Parser_Command_preterm___elambda__1___rarg(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; obj* x_4; obj* x_5; obj* x_15; obj* x_16; obj* x_17; 
+x_3 = lean::cnstr_get(x_2, 0);
+lean::inc(x_3);
+x_4 = lean::array_get_size(x_3);
+lean::dec(x_3);
+x_15 = lean::cnstr_get(x_2, 1);
+lean::inc(x_15);
+lean::inc(x_1);
+x_16 = l_Lean_Parser_tokenFn(x_1, x_2);
+x_17 = lean::cnstr_get(x_16, 3);
+lean::inc(x_17);
+if (lean::obj_tag(x_17) == 0)
+{
+obj* x_18; obj* x_19; 
+x_18 = lean::cnstr_get(x_16, 0);
+lean::inc(x_18);
+x_19 = l_Array_back___at___private_init_lean_parser_parser_6__updateCache___spec__1(x_18);
+lean::dec(x_18);
+if (lean::obj_tag(x_19) == 2)
+{
+obj* x_20; obj* x_21; uint8 x_22; 
+x_20 = lean::cnstr_get(x_19, 1);
+lean::inc(x_20);
+lean::dec(x_19);
+x_21 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4;
+x_22 = lean::string_dec_eq(x_20, x_21);
+lean::dec(x_20);
+if (x_22 == 0)
+{
+obj* x_23; obj* x_24; 
+x_23 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7;
+x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_23, x_15);
+x_5 = x_24;
+goto block_14;
+}
+else
+{
+lean::dec(x_15);
+x_5 = x_16;
+goto block_14;
+}
+}
+else
+{
+obj* x_25; obj* x_26; 
+lean::dec(x_19);
+x_25 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7;
+x_26 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_25, x_15);
+x_5 = x_26;
+goto block_14;
+}
+}
+else
+{
+obj* x_27; obj* x_28; 
+lean::dec(x_17);
+x_27 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7;
+x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_27, x_15);
+x_5 = x_28;
+goto block_14;
+}
+block_14:
+{
+obj* x_6; 
+x_6 = lean::cnstr_get(x_5, 3);
+lean::inc(x_6);
+if (lean::obj_tag(x_6) == 0)
+{
+obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
+x_7 = l_Lean_Parser_termParserAttribute;
+x_8 = lean::mk_nat_obj(0u);
+x_9 = l_Lean_Parser_ParserAttribute_runParser(x_7, x_8, x_1, x_5);
+x_10 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
+x_11 = l_Lean_Parser_ParserState_mkNode(x_9, x_10, x_4);
+return x_11;
+}
+else
+{
+obj* x_12; obj* x_13; 
+lean::dec(x_6);
+lean::dec(x_1);
+x_12 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
+x_13 = l_Lean_Parser_ParserState_mkNode(x_5, x_12, x_4);
+return x_13;
+}
+}
+}
+}
+obj* l_Lean_Parser_Command_preterm___elambda__1(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Command_preterm___elambda__1___rarg), 2, 0);
+return x_2;
+}
+}
+obj* _init_l_Lean_Parser_Command_preterm___closed__1() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = lean::box(0);
+x_2 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4;
+x_3 = l_Lean_Parser_symbolInfo(x_2, x_1);
+return x_3;
+}
+}
+obj* _init_l_Lean_Parser_Command_preterm___closed__2() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Command_preterm___closed__1;
+x_2 = l_Lean_Parser_Parser_inhabited___closed__1;
+x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
+return x_3;
+}
+}
+obj* _init_l_Lean_Parser_Command_preterm___closed__3() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
+x_2 = l_Lean_Parser_Command_preterm___closed__2;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
+}
+}
+obj* _init_l_Lean_Parser_Command_preterm___closed__4() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Command_preterm___elambda__1___boxed), 1, 0);
+return x_1;
+}
+}
+obj* _init_l_Lean_Parser_Command_preterm___closed__5() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Command_preterm___closed__3;
+x_2 = l_Lean_Parser_Command_preterm___closed__4;
+x_3 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_3, 0, x_1);
+lean::cnstr_set(x_3, 1, x_2);
+return x_3;
+}
+}
+obj* _init_l_Lean_Parser_Command_preterm() {
+_start:
+{
+obj* x_1; 
+x_1 = l_Lean_Parser_Command_preterm___closed__5;
+return x_1;
+}
+}
+obj* l_Lean_Parser_Command_preterm___elambda__1___boxed(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Lean_Parser_Command_preterm___elambda__1(x_1);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l___regBuiltinParser_Lean_Parser_Command_preterm(obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; obj* x_4; obj* x_5; 
+x_2 = l_Lean_Parser_builtinCommandParsingTable;
+x_3 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
+x_4 = l_Lean_Parser_Command_preterm;
+x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
 obj* _init_l_Lean_Parser_Command_init__quot___elambda__1___rarg___closed__1() {
 _start:
 {
@@ -24147,6 +24408,34 @@ l_Lean_Parser_Command_resolve__name = _init_l_Lean_Parser_Command_resolve__name(
 lean::mark_persistent(l_Lean_Parser_Command_resolve__name);
 w = l___regBuiltinParser_Lean_Parser_Command_resolve__name(w);
 if (io_result_is_error(w)) return w;
+l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__1 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__1();
+lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__1);
+l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2();
+lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2);
+l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__3 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__3();
+lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__3);
+l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4();
+lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4);
+l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__5 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__5();
+lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__5);
+l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6();
+lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6);
+l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7();
+lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7);
+l_Lean_Parser_Command_preterm___closed__1 = _init_l_Lean_Parser_Command_preterm___closed__1();
+lean::mark_persistent(l_Lean_Parser_Command_preterm___closed__1);
+l_Lean_Parser_Command_preterm___closed__2 = _init_l_Lean_Parser_Command_preterm___closed__2();
+lean::mark_persistent(l_Lean_Parser_Command_preterm___closed__2);
+l_Lean_Parser_Command_preterm___closed__3 = _init_l_Lean_Parser_Command_preterm___closed__3();
+lean::mark_persistent(l_Lean_Parser_Command_preterm___closed__3);
+l_Lean_Parser_Command_preterm___closed__4 = _init_l_Lean_Parser_Command_preterm___closed__4();
+lean::mark_persistent(l_Lean_Parser_Command_preterm___closed__4);
+l_Lean_Parser_Command_preterm___closed__5 = _init_l_Lean_Parser_Command_preterm___closed__5();
+lean::mark_persistent(l_Lean_Parser_Command_preterm___closed__5);
+l_Lean_Parser_Command_preterm = _init_l_Lean_Parser_Command_preterm();
+lean::mark_persistent(l_Lean_Parser_Command_preterm);
+w = l___regBuiltinParser_Lean_Parser_Command_preterm(w);
+if (io_result_is_error(w)) return w;
 l_Lean_Parser_Command_init__quot___elambda__1___rarg___closed__1 = _init_l_Lean_Parser_Command_init__quot___elambda__1___rarg___closed__1();
 lean::mark_persistent(l_Lean_Parser_Command_init__quot___elambda__1___rarg___closed__1);
 l_Lean_Parser_Command_init__quot___elambda__1___rarg___closed__2 = _init_l_Lean_Parser_Command_init__quot___elambda__1___rarg___closed__2();