feat(library/init/lean): implement init_quot

library/init/lean/elaborator.lean

@@ -750,6 +750,9 @@ def export.elaborate : elaborator :=
   -- TODO: do eager sanity checks (namespace does not exist, etc.)
   modify $ λ st, {st with export_decls := st.export_decls ++ v.spec.map (λ spec, ⟨ns, spec⟩)}
 
+def init_quot.elaborate : elaborator :=
+λ stx, old_elab_command stx $ expr.mdata (kvmap.set_name {} `command `init_quot) dummy
+
 /-- List of commands: recursively elaborate each command. -/
 def no_kind.elaborate : coelaborator := do
   stx ← current_command,
@@ -821,7 +824,8 @@ def elaborators : rbmap name coelaborator (<) := rbmap.from_list [
   (attribute.name, attribute.elaborate),
   (open.name, open.elaborate),
   (export.name, export.elaborate),
-  (check.name, check.elaborate)
+  (check.name, check.elaborate),
+  (init_quot.name, init_quot.elaborate)
 ] _
 
 def resolve_global : name → elaborator_m (list name)

library/init/lean/parser/command.lean

@@ -93,12 +93,16 @@ node! «attribute» [
   ids: ident.parser*
 ]
 
+@[derive parser.has_tokens parser.has_view]
+def init_quot.parser : command_parser :=
+node! «init_quot» ["init_quot"]
+
 @[derive has_tokens]
 def builtin_command_parsers : list command_parser := [
   declaration.parser, variable.parser, variables.parser, namespace.parser, end.parser,
   open.parser, section.parser, universe.parser, notation.parser, reserve_notation.parser,
   mixfix.parser, reserve_mixfix.parser, check.parser, attribute.parser,
-  export.parser, include.parser, omit.parser]
+  export.parser, include.parser, omit.parser, init_quot.parser]
 end «command»
 
 def command_parser.run (commands : list command_parser) (p : command_parser)

src/frontends/lean/vm_elaborator.cpp

@@ -318,6 +318,9 @@ static void elaborate_command(parser & p, expr const & cmd) {
         } else if (*cmd_name == "structure") {
             elab_structure_cmd(p, cmd);
             return;
+        } else if (*cmd_name == "init_quot") {
+            p.set_env(module::add(p.env(), mk_quot_decl()));
+            return;
         }
     }
     throw elaborator_exception(cmd, "unexpected input to 'elaborate_command'");