chore: update stage0

stage0/src/Init/Lean/Elab/Quotation.lean

@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+prelude
+import Init.Lean.Syntax
+import Init.Lean.Elab.ResolveName
+import Init.Lean.Parser -- TODO: remove after removing old elaborator
+
+namespace Lean
+namespace Elab
+
+-- TODO: replace with quotations where possible
+private def const (n : Name) : Syntax :=
+Syntax.node `Lean.Parser.Term.id #[Syntax.ident none n.toString.toSubstring n [(n, [])]]
+
+private def app (fn arg : Syntax) : Syntax :=
+Syntax.node `Lean.Parser.Term.app #[fn, arg]
+
+private def appN (fn : Syntax) (args : Array Syntax) : Syntax :=
+args.foldl app fn
+
+-- TODO: unclear if the following functions could also be useful to other code
+private def quoteName : Name → Syntax
+| Name.anonymous => const `Lean.Name.anonymous
+| Name.str n s _ => appN (const `Lean.mkNameStr) #[quoteName n, mkStxStrLit s]
+| Name.num n i _ => appN (const `Lean.mkNameNum) #[quoteName n, mkStxNumLit $ toString i]
+
+private def quoteList : List Syntax → Syntax
+| [] => const `List.nil
+| (x::xs) => appN (const `List.cons) #[x, quoteList xs]
+
+private def quoteArray : Array Syntax → Syntax
+| xs => app (const `List.toArray) $ quoteList xs.toList
+
+private partial def quote (env : Environment) (msc : Syntax) : Syntax → Syntax
+| Syntax.ident info rawVal val preresolved =>
+  -- TODO: pass scope information
+  let ns := Name.anonymous;
+  let openDecls := [];
+  let preresolved := resolveGlobalName env ns openDecls val <|> preresolved;
+  --`(Syntax.ident none (String.toSubstring %(rawVal.toString)) (Name.mkNumeral %val %msc))
+  appN (const `Lean.Syntax.ident) #[
+    const `Option.none,
+    app (const `String.toSubstring) (mkStxStrLit rawVal.toString),
+    --appN (const `Lean.Name.mkNumeral) #[quoteName val, msc]
+    -- TODO: hygiene
+    quoteName val,
+    quoteList $ preresolved.map $ fun ⟨n, ss⟩ => appN (const `Prod.mk) #[quoteName n, quoteList $ ss.map mkStxStrLit]
+  ]
+| Syntax.node `Lean.Parser.Term.antiquot args => args.get! 1
+| Syntax.node k args =>
+  --`(Syntax.node %k %args...)
+  let args := quoteArray $ args.map quote;
+  appN (const `Lean.Syntax.node) $ #[quoteName k, args]
+| Syntax.atom info val => --`(Syntax.atom none %val)
+  appN (const `Lean.Syntax.atom) #[
+    const `Option.none,
+    mkStxStrLit val
+  ]
+| Syntax.missing => unreachable!
+
+-- TODO: hygiene
+def stxQuot.expand (env : Environment) (stx : Syntax) : Syntax :=
+-- `(do msc ← getCurMacroScope; pure %(quote `(msc) quoted))
+app (const `HasPure.pure) $ quote env Syntax.missing $ stx.getArg 1
+
+-- REMOVE with old frontend
+private partial def toPreterm (env : Environment) : Syntax → Except String Expr
+| stx =>
+  let args := stx.getArgs;
+  match stx.getKind with
+  | `Lean.Parser.Term.id =>
+    match args.get! 0 with
+    | Syntax.ident _ _ val preresolved =>
+      -- TODO: pass scope information
+      let ns := Name.anonymous;
+      let openDecls := [];
+      let resolved := resolveGlobalName env ns openDecls val <|> preresolved;
+      match resolved with
+      | (pre,[])::_ => pure $ mkConst pre
+      | [] => pure $ mkFVar val
+      | _ => throw "stxQuot: unimplemented: projection notation"
+    | _ => unreachable!
+  | `Lean.Parser.Term.app => do
+    fn ← toPreterm $ args.get! 0;
+    arg ← toPreterm $ args.get! 1;
+    pure $ mkApp fn arg
+  | `Lean.Parser.Term.paren => toPreterm $ (args.get! 1).getArg 0
+  | `strLit => pure $ mkStrLit $ stx.isStrLit.getD ""
+  | `numLit => pure $ mkNatLit $ stx.isNatLit.getD 0
+  | k => panic! "stxQuot: unimplemented kind " ++ toString k
+
+@[export lean_parse_stx_quot]
+def oldParseStxQuot (env : Environment) (input : String) (pos : String.Pos) : Except String (Expr × String.Pos) := do
+  let c := Parser.mkParserContextCore env input "<foo>";
+  let c := c.toParserContext env;
+  let s := Parser.mkParserState c.input;
+  let s := s.setPos pos;
+  let s := (Parser.termParser : Parser.Parser).fn (0 : Nat) c s;
+  let stx := s.stxStack.back;
+  let stx := app (const `HasPure.pure) $ quote env Syntax.missing stx;
+  expr ← toPreterm env stx;
+  match s.errorMsg with
+  | some errorMsg =>
+    Except.error $ toString errorMsg
+  | none =>
+    Except.ok (expr, s.pos)
+
+end Elab
+end Lean

stage0/src/Init/Lean/Elab/Term.lean

@@ -8,6 +8,7 @@ import Init.Lean.Meta
 import Init.Lean.Elab.Log
 import Init.Lean.Elab.Alias
 import Init.Lean.Elab.ResolveName
+import Init.Lean.Elab.Quotation
 
 namespace Lean
 namespace Elab
@@ -164,6 +165,11 @@ fun _ expectedType? =>
   | some expectedType => mkFreshExprMVar expectedType
   | none              => do u ← mkFreshLevelMVar; mkFreshExprMVar (mkSort u)
 
+@[builtinTermElab stxQuot] def elabStxQuot : TermElab :=
+fun stx expectedType? => do
+  env ← getEnv;
+  elabTerm (stxQuot.expand env (stx.getArg 1)) expectedType?
+
 private def mkFreshAnonymousName : TermElabM Name :=
 do s ← get;
    let anonymousIdx := s.anonymousIdx;

stage0/src/frontends/lean/builtin_exprs.cpp

@@ -821,6 +821,21 @@ static expr parse_trace(parser & p, unsigned, expr const *, pos_info const & pos
     return save_pos(r, pos);
 }
 
+extern "C" object * lean_parse_stx_quot(object * env, object * input, object * pos);
+
+static expr parse_stx_quot(parser & p, unsigned, expr const *, pos_info const & pos) {
+    object_ref r(lean_parse_stx_quot(p.env().to_obj_arg(), mk_string(p.m_scanner.m_curr_line), nat(p.m_scanner.m_spos).to_obj_arg()));
+    if (cnstr_tag(r.raw()) == 0) {
+        throw parser_error(sstream() << cnstr_get_ref_t<string_ref>(r, 0).to_std_string(), p.pos());
+    } else {
+        object_ref tup = cnstr_get_ref(r, 0);
+        p.m_scanner.skip_to_pos(pos_info {0, cnstr_get_ref_t<nat>(tup, 1).get_small_value()});
+        p.next();
+        p.check_token_next(get_rparen_tk(), "')' expected");
+        return cnstr_get_ref_t<expr>(tup, 0);
+    }
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -859,6 +874,7 @@ parse_table init_nud_table() {
     r = r.add({transition("tparser!", mk_ext_action(parse_tparser))}, x0);
     r = r.add({transition("panic!", mk_ext_action(parse_panic))}, x0);
     r = r.add({transition("trace!", mk_ext_action(parse_trace))}, x0);
+    r = r.add({transition("`(", mk_ext_action_core(parse_stx_quot))}, x0);
     return r;
 }
 

stage0/src/frontends/lean/scanner.cpp

@@ -710,7 +710,7 @@ void scanner::skip_to_pos(pos_info const & pos) {
     for (unsigned line_no = 1; line_no < pos.first; line_no++)
         fetch_line();
     m_line = m_sline;
-    while (static_cast<unsigned>(m_upos) < pos.second)
+    while (static_cast<unsigned>(m_spos) < pos.second)
         next();
     m_pos = m_upos; // we assume that the argument is the start of a token
     // lean_assert(pos == pos_info(get_line(), get_pos()));

stage0/src/frontends/lean/scanner.h

@@ -29,7 +29,7 @@ enum class token_kind {Keyword, CommandKeyword, Identifier, Numeral, Decimal,
     accepted if they are in the token set.
 */
 class scanner {
-protected:
+public:
     token_table const * m_tokens;
     std::istream *      m_stream;
     std::string         m_stream_name;

stage0/stdlib/Init/Lean/Elab/Term.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Elab.Term
-// Imports: Init.Lean.Meta Init.Lean.Elab.Log Init.Lean.Elab.Alias Init.Lean.Elab.ResolveName
+// Imports: Init.Lean.Meta Init.Lean.Elab.Log Init.Lean.Elab.Alias Init.Lean.Elab.ResolveName Init.Lean.Elab.Quotation
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -35,6 +35,7 @@ lean_object* l_Lean_Elab_Term_TermElabM_monadLog___closed__3;
 lean_object* l_Lean_Elab_Term_tracer___closed__5;
 lean_object* l_Lean_Elab_Term_mkFreshExprMVar(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_2__mkFreshInstanceName(lean_object*);
+lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__2;
 extern lean_object* l_Lean_nameToExprAux___main___closed__1;
 lean_object* l_unreachable_x21___rarg(lean_object*);
 lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__1;
@@ -42,6 +43,7 @@ extern lean_object* l_Lean_nullKind;
 lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__8;
 lean_object* l_Nat_foldMAux___main___at___private_Init_Lean_Elab_Term_11__mkFreshLevelMVars___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabHole___rarg(lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteList___main___closed__4;
 lean_object* l_Lean_Elab_Term_elabDepArrow(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__2;
 lean_object* l_Lean_Elab_Term_elabArrow___closed__1;
@@ -75,6 +77,7 @@ extern lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_TermElabM_monadLog___lambda__4___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Log_1__resetTraceState___at_Lean_Elab_Term_elabTerm___spec__7(lean_object*);
 extern lean_object* l_Prod_HasRepr___rarg___closed__1;
+lean_object* l_Lean_Elab_Term_elabStxQuot___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_TermElabM_monadLog___closed__6;
 lean_object* l___private_Init_Lean_Elab_Log_1__resetTraceState___at_Lean_Elab_Term_elabTerm___spec__7___rarg(lean_object*);
 extern lean_object* l_Lean_stxInh;
@@ -100,6 +103,7 @@ uint8_t lean_name_eq(lean_object*, lean_object*);
 lean_object* lean_io_ref_get(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__5;
 lean_object* l_Lean_Elab_Term_registerBuiltinTermElabAttr___closed__6;
+lean_object* l_Lean_Elab_stxQuot_expand(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Util_Trace_4__checkTraceOption___at_Lean_Elab_Term_elabTerm___spec__13___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHole(lean_object*);
@@ -133,7 +137,6 @@ lean_object* l_PersistentHashMap_findAux___main___at_Lean_Elab_Term_elabTerm___s
 lean_object* l_Lean_Elab_Term_elabTypeStx___rarg(lean_object*);
 lean_object* l_Lean_mkAtom(lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabTypeStx___closed__1;
-extern lean_object* l_Lean_Parser_Term_cons___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Term_TermElabM_monadLog___closed__2;
 lean_object* l_Lean_Elab_Term_dbgTrace___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_FileMap_ofString___closed__1;
@@ -159,7 +162,6 @@ lean_object* l_Lean_Elab_Term_whnf(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_getOptions(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_prop___elambda__1___rarg___closed__2;
 lean_object* l_Lean_Elab_Term_elabParen___closed__1;
-lean_object* l_Lean_Elab_Term_elabListLit___closed__1;
 lean_object* l_Lean_Elab_Term_liftMetaM(lean_object*);
 extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__1;
 lean_object* l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Elab_Term_elabListLit___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -171,7 +173,6 @@ lean_object* l___private_Init_Lean_Elab_Term_4__expandBinderIdent(lean_object*,
 lean_object* l___private_Init_Lean_Elab_Term_7__elabBinderViews___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_SMap_contains___at_Lean_Elab_Term_addBuiltinTermElab___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_Elab_Term_addBuiltinTermElab___spec__10(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_elabListLit___closed__2;
 extern lean_object* l_Lean_Meta_dbgTrace___rarg___closed__1;
 lean_object* l___private_Init_Lean_Elab_Term_12__mkConsts(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_4__expandBinderIdent___boxed(lean_object*, lean_object*, lean_object*);
@@ -215,8 +216,10 @@ lean_object* l___private_Init_Lean_Elab_Term_3__expandBinderType___boxed(lean_ob
 lean_object* l_Lean_Elab_Term_elabForall___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__6;
 lean_object* l_Lean_Elab_mkElabAttribute___rarg___lambda__2___boxed(lean_object*, lean_object*);
+lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__1;
 lean_object* l_Lean_Elab_Term_TermElabM_monadLog___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___rarg___closed__2;
 lean_object* l_Lean_Elab_Term_setTraceState___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
 lean_object* l_Lean_Elab_Term_registerBuiltinTermElabAttr___closed__7;
@@ -241,7 +244,6 @@ lean_object* l_Lean_Elab_Term_withNode___rarg___closed__2;
 lean_object* l___private_Init_Lean_Elab_Term_7__elabBinderViews___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabListLit___closed__3;
 lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Elab_Term_mkTermElabAttribute___spec__4(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_elabListLit___closed__4;
 extern lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__2;
 extern lean_object* l_PersistentHashMap_insertAux___main___rarg___closed__3;
 lean_object* l_Lean_Syntax_getId(lean_object*);
@@ -302,6 +304,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSort___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabApp(lean_object*);
 lean_object* l_Lean_Elab_Term_addBuiltinTermElab___closed__1;
 lean_object* l___private_Init_Lean_Elab_Term_2__mkFreshInstanceName___rarg(lean_object*);
+lean_object* l_Lean_Elab_Term_elabStxQuot(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_mkHashMapImp___rarg(lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabParen___closed__1;
 lean_object* l_Lean_Elab_Term_addBuiltinTermElab___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -317,7 +320,6 @@ lean_object* l_Lean_mkFVar(lean_object*);
 extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__3;
 lean_object* l_Lean_ConstantInfo_type(lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabProp___closed__1;
-lean_object* l_Lean_Elab_Term_elabListLit___closed__5;
 lean_object* l_Lean_Elab_Term_elabBinders___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 size_t l_USize_land(size_t, size_t);
 lean_object* l_HashMapImp_contains___at_Lean_Elab_Term_addBuiltinTermElab___spec__2___boxed(lean_object*, lean_object*);
@@ -358,6 +360,7 @@ lean_object* l_Lean_Elab_Term_elabApp___boxed(lean_object*, lean_object*, lean_o
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabForall___closed__3;
 extern lean_object* l_Lean_Parser_Term_instBinder___elambda__1___rarg___closed__2;
 lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
+extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteList___main___closed__6;
 lean_object* l_Array_iterateMAux___main___at_Lean_mkAppStx___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__5;
 lean_object* l_Lean_Elab_Term_getLCtx(lean_object*, lean_object*);
@@ -462,6 +465,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabDepArrow___closed__2;
 lean_object* l_Lean_Elab_Term_mkFreshLevelMVar(lean_object*);
 lean_object* l_Lean_Elab_Term_tracer___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__4;
+lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__3;
 lean_object* l_Lean_Elab_Term_resettingSynthInstanceCache___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* lean_io_initializing(lean_object*);
 lean_object* l_Lean_Elab_mkMessage___at_Lean_Elab_Term_elabTerm___spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -472,6 +476,7 @@ lean_object* l_Lean_Elab_Term_resolveName___closed__2;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabApp___closed__1;
 lean_object* l_Lean_Elab_Term_getLCtx___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkFreshLevelMVar___boxed(lean_object*);
+lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot(lean_object*);
 uint8_t l___private_Init_Lean_Util_Trace_3__checkTraceOptionAux___main(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_logAt___at_Lean_Elab_Term_elabTerm___spec__10(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_setTraceState(lean_object*, lean_object*, lean_object*);
@@ -479,7 +484,6 @@ lean_object* l_Lean_Elab_logErrorAndThrow___at_Lean_Elab_Term_resolveName___spec
 lean_object* l_Lean_Meta_mkFreshLevelMVar___rarg(lean_object*);
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 uint8_t l_Lean_SMap_contains___at_Lean_Elab_Term_addBuiltinTermElab___spec__1(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_elabListLit___closed__3;
 lean_object* l_Lean_Elab_Term_addContext(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_registerBuiltinTermElabAttr___closed__4;
@@ -7777,6 +7781,73 @@ x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
+lean_object* l_Lean_Elab_Term_elabStxQuot(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+x_5 = l_Lean_Elab_Term_getEnv___rarg(x_4);
+x_6 = lean_ctor_get(x_5, 0);
+lean_inc(x_6);
+x_7 = lean_ctor_get(x_5, 1);
+lean_inc(x_7);
+lean_dec(x_5);
+x_8 = lean_ctor_get(x_1, 1);
+x_9 = l_Lean_stxInh;
+x_10 = lean_unsigned_to_nat(1u);
+x_11 = lean_array_get(x_9, x_8, x_10);
+x_12 = l_Lean_Elab_stxQuot_expand(x_6, x_11);
+lean_dec(x_11);
+lean_dec(x_6);
+x_13 = l_Lean_Elab_Term_elabTerm(x_12, x_2, x_3, x_7);
+return x_13;
+}
+}
+lean_object* l_Lean_Elab_Term_elabStxQuot___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_Elab_Term_elabStxQuot(x_1, x_2, x_3, x_4);
+lean_dec(x_1);
+return x_5;
+}
+}
+lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("elabStxQuot");
+return x_1;
+}
+}
+lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Elab_Term_declareBuiltinTermElab___closed__4;
+x_2 = l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__3() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabStxQuot___boxed), 4, 0);
+return x_1;
+}
+}
+lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Parser_Term_stxQuot___elambda__1___rarg___closed__2;
+x_3 = l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__2;
+x_4 = l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__3;
+x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
 lean_object* _init_l___private_Init_Lean_Elab_Term_1__mkFreshAnonymousName___rarg___closed__1() {
 _start:
 {
@@ -17628,52 +17699,6 @@ goto _start;
 }
 }
 }
-lean_object* _init_l_Lean_Elab_Term_elabListLit___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string("List");
-return x_1;
-}
-}
-lean_object* _init_l_Lean_Elab_Term_elabListLit___closed__2() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = lean_box(0);
-x_2 = l_Lean_Elab_Term_elabListLit___closed__1;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Elab_Term_elabListLit___closed__3() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Elab_Term_elabListLit___closed__2;
-x_2 = l_Lean_Parser_Term_cons___elambda__1___closed__1;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Elab_Term_elabListLit___closed__4() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string("nil");
-return x_1;
-}
-}
-lean_object* _init_l_Lean_Elab_Term_elabListLit___closed__5() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Elab_Term_elabListLit___closed__2;
-x_2 = l_Lean_Elab_Term_elabListLit___closed__4;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
 lean_object* l_Lean_Elab_Term_elabListLit(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
@@ -17682,7 +17707,7 @@ x_5 = lean_ctor_get(x_1, 1);
 x_6 = l_Lean_stxInh;
 x_7 = lean_unsigned_to_nat(0u);
 x_8 = lean_array_get(x_6, x_5, x_7);
-x_9 = l_Lean_Elab_Term_elabListLit___closed__3;
+x_9 = l___private_Init_Lean_Elab_Quotation_5__quoteList___main___closed__6;
 x_10 = l_Lean_mkIdentFrom(x_8, x_9);
 lean_dec(x_8);
 x_11 = lean_unsigned_to_nat(1u);
@@ -17691,7 +17716,7 @@ x_13 = l_Lean_Syntax_getArgs(x_12);
 lean_dec(x_12);
 x_14 = lean_unsigned_to_nat(2u);
 x_15 = lean_array_get(x_6, x_5, x_14);
-x_16 = l_Lean_Elab_Term_elabListLit___closed__5;
+x_16 = l___private_Init_Lean_Elab_Quotation_5__quoteList___main___closed__4;
 x_17 = l_Lean_mkIdentFrom(x_15, x_16);
 lean_dec(x_15);
 x_18 = l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Elab_Term_elabListLit___spec__1(x_10, x_14, x_13, x_7, x_17);
@@ -19156,6 +19181,7 @@ lean_object* initialize_Init_Lean_Meta(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Log(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Alias(lean_object*);
 lean_object* initialize_Init_Lean_Elab_ResolveName(lean_object*);
+lean_object* initialize_Init_Lean_Elab_Quotation(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean_Elab_Term(lean_object* w) {
 lean_object * res;
@@ -19173,6 +19199,9 @@ lean_dec_ref(res);
 res = initialize_Init_Lean_Elab_ResolveName(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Elab_Quotation(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 l_Lean_Elab_Term_TermElabM_monadLog___closed__1 = _init_l_Lean_Elab_Term_TermElabM_monadLog___closed__1();
 lean_mark_persistent(l_Lean_Elab_Term_TermElabM_monadLog___closed__1);
 l_Lean_Elab_Term_TermElabM_monadLog___closed__2 = _init_l_Lean_Elab_Term_TermElabM_monadLog___closed__2();
@@ -19332,6 +19361,15 @@ lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabHole___closed__3)
 res = l___regBuiltinTermElab_Lean_Elab_Term_elabHole(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__1();
+lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__1);
+l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__2();
+lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__2);
+l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__3();
+lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__3);
+res = l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 l___private_Init_Lean_Elab_Term_1__mkFreshAnonymousName___rarg___closed__1 = _init_l___private_Init_Lean_Elab_Term_1__mkFreshAnonymousName___rarg___closed__1();
 lean_mark_persistent(l___private_Init_Lean_Elab_Term_1__mkFreshAnonymousName___rarg___closed__1);
 l___private_Init_Lean_Elab_Term_1__mkFreshAnonymousName___rarg___closed__2 = _init_l___private_Init_Lean_Elab_Term_1__mkFreshAnonymousName___rarg___closed__2();
@@ -19412,16 +19450,6 @@ lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabParen___closed__3
 res = l___regBuiltinTermElab_Lean_Elab_Term_elabParen(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-l_Lean_Elab_Term_elabListLit___closed__1 = _init_l_Lean_Elab_Term_elabListLit___closed__1();
-lean_mark_persistent(l_Lean_Elab_Term_elabListLit___closed__1);
-l_Lean_Elab_Term_elabListLit___closed__2 = _init_l_Lean_Elab_Term_elabListLit___closed__2();
-lean_mark_persistent(l_Lean_Elab_Term_elabListLit___closed__2);
-l_Lean_Elab_Term_elabListLit___closed__3 = _init_l_Lean_Elab_Term_elabListLit___closed__3();
-lean_mark_persistent(l_Lean_Elab_Term_elabListLit___closed__3);
-l_Lean_Elab_Term_elabListLit___closed__4 = _init_l_Lean_Elab_Term_elabListLit___closed__4();
-lean_mark_persistent(l_Lean_Elab_Term_elabListLit___closed__4);
-l_Lean_Elab_Term_elabListLit___closed__5 = _init_l_Lean_Elab_Term_elabListLit___closed__5();
-lean_mark_persistent(l_Lean_Elab_Term_elabListLit___closed__5);
 l___regBuiltinTermElab_Lean_Elab_Term_elabListLit___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabListLit___closed__1();
 lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabListLit___closed__1);
 l___regBuiltinTermElab_Lean_Elab_Term_elabListLit___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabListLit___closed__2();