chore: update stage0

stage0/src/Init/Lean/Elab.lean

@@ -15,3 +15,4 @@ import Init.Lean.Elab.Quotation
 import Init.Lean.Elab.Frontend
 import Init.Lean.Elab.BuiltinNotation
 import Init.Lean.Elab.Declaration
+import Init.Lean.Elab.Tactic

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

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+prelude
+import Init.Lean.Elab.Term
+
+namespace Lean
+namespace Elab
+namespace Term
+
+@[builtinTermElab tacticBlock] def elabTacticBlock : TermElab :=
+fun stx _ =>
+  throwError stx ("not implemented yet " ++ stx)
+
+end Term
+
+end Elab
+end Lean

stage0/src/Init/Lean/Parser/Parser.lean

@@ -1231,6 +1231,41 @@ structure ParsingTables :=
 
 instance ParsingTables.inhabited : Inhabited ParsingTables := ⟨{}⟩
 
+/-
+  Each parser category has its own Pratt's parsing tables.
+  The system comes equipped with the following categories: `level`, `term`, `tactic`, and `command`.
+  Users and plugins may define extra categories.
+
+  The field `leadingIdentAsSymbol` specifies how the parsing table lookup function behaves for identifiers.
+  The function `prattParser` uses two tables `leadingTable` and `trailingTable`. They map tokens to
+  parsers. If `leadingIdentAsSymbol == false` and the leading token is an identifier, then `prattParser`
+  just executes the parsers associated with the auxiliary token "ident".
+  If `leadingIdentAsSymbol == true` and the leading token is an identifier `<foo>`, then `prattParser`
+  combines the parsers associated with the token `<foo>` with the parsers associated with the auxiliary token "ident".
+  We use this feature and a variant of the `nonReservedSymbol` parser to implement the `tactic` parsers.
+  We use this approach to avoid creating a reserved symbol for each builtin tactic (e.g., `apply`, `assumption`, etc.).
+  That is, users may still use these symbols as identifiers (e.g., naming a function).
+-/
+structure ParserCategory :=
+(tables               : ParsingTables)
+(leadingIdentAsSymbol : Bool := false)
+
+abbrev ParserCategories := PersistentHashMap Name ParserCategory
+
+def tacticSymbolInfo (sym : String) : ParserInfo :=
+{ firstTokens  := FirstTokens.tokens [ { val := sym } ] }
+
+/-
+  Variant of `nonReservedSymbol sym` which only register this parser as a leading parser with first token `sym`.
+  This parser only makes sense for categories that set `leadingIdentAsSymbol == true`, as the `tactic` category.
+
+  TODO: when defining convenient notation for writing new tactics, we should use `tacticSymbol` instead of `symbol`.
+-/
+@[inline] def tacticSymbol (sym : String) : Parser :=
+let sym := sym.trim;
+{ info := tacticSymbolInfo sym,
+  fn   := fun _ => nonReservedSymbolFn sym }
+
 def currLbp (left : Syntax) (c : ParserContext) (s : ParserState) : ParserState × Nat :=
 let (s, stx) := peekToken c s;
 match stx with
@@ -1258,7 +1293,9 @@ match stx with
 | some (Syntax.ident _ _ val _) =>
   if leadingIdentAsSymbol then
     match map.find val with
-    | some as => (s, as)
+    | some as => match map.find `ident with
+      | some as' => (s, as ++ as')
+      | _        => (s, as)
     | none    => find `ident
   else
     find `ident
@@ -1338,12 +1375,6 @@ def mkBuiltinTokenTable : IO (IO.Ref TokenTable) := IO.mkRef {}
 def mkBuiltinSyntaxNodeKindSetRef : IO (IO.Ref SyntaxNodeKindSet) := IO.mkRef {}
 @[init mkBuiltinSyntaxNodeKindSetRef] constant builtinSyntaxNodeKindSetRef : IO.Ref SyntaxNodeKindSet := arbitrary _
 
-structure ParserCategory :=
-(tables               : ParsingTables)
-(leadingIdentAsSymbol : Bool := false)
-
-abbrev ParserCategories := PersistentHashMap Name ParserCategory
-
 def mkBuiltinParserCategories : IO (IO.Ref ParserCategories) := IO.mkRef {}
 @[init mkBuiltinParserCategories] constant builtinParserCategoriesRef : IO.Ref ParserCategories := arbitrary _
 
@@ -1493,6 +1524,7 @@ def compileParserDescr (categories : ParserCategories) : forall {k : ParserKind}
 | _, ParserDescr.sepBy1 d₁ d₂                        => sepBy1 <$> compileParserDescr d₁ <*> compileParserDescr d₂
 | _, ParserDescr.node k d                            => node k <$> compileParserDescr d
 | _, ParserDescr.symbol tk lbp                       => pure $ symbol tk lbp
+| ParserKind.leading, ParserDescr.tacticSymbol tk    => pure $ tacticSymbol tk
 | _, ParserDescr.unicodeSymbol tk₁ tk₂ lbp           => pure $ unicodeSymbol tk₁ tk₂ lbp
 | ParserKind.leading, ParserDescr.parser catName rbp =>
   match categories.find? catName with

stage0/src/Init/Lean/Parser/Tactic.lean

@@ -10,7 +10,8 @@ namespace Lean
 namespace Parser
 
 @[init] def regBuiltinTacticParserAttr : IO Unit :=
-registerBuiltinParserAttribute `builtinTacticParser `tactic
+let leadingIdentAsSymbol := true;
+registerBuiltinParserAttribute `builtinTacticParser `tactic leadingIdentAsSymbol
 
 @[init] def regTacticParserAttribute : IO Unit :=
 registerBuiltinDynamicParserAttribute `tacticParser `tactic
@@ -23,14 +24,6 @@ sepBy1 tacticParser "; " true
 
 namespace Tactic
 
-def tacticSymbolInfo (sym : String) : ParserInfo :=
-{ firstTokens  := FirstTokens.tokens [ { val := sym } ] }
-
-@[inline] def tacticSymbol {k : ParserKind} (sym : String) : Parser k :=
-let sym := sym.trim;
-{ info := tacticSymbolInfo sym,
-  fn   := fun _ => nonReservedSymbolFn sym }
-
 @[builtinTacticParser] def «intro» := parser! tacticSymbol "intro " >> optional ident
 @[builtinTacticParser] def «intros» := parser! tacticSymbol "intros " >> many ident
 @[builtinTacticParser] def «assumption» := parser! tacticSymbol "assumption"

stage0/src/Init/LeanExt.lean

@@ -42,6 +42,7 @@ inductive ParserDescrCore : ParserKind → Type
 | node {k : ParserKind}          : Name → ParserDescrCore k → ParserDescrCore k
 | symbol {k : ParserKind}        : String → Nat → ParserDescrCore k
 | unicodeSymbol {k : ParserKind} : String → String → Nat → ParserDescrCore k
+| tacticSymbol                   : String → ParserDescrCore ParserKind.leading
 | pushLeading                    : ParserDescrCore ParserKind.trailing
 | parser                         : Name → Nat → ParserDescrCore ParserKind.leading
 
@@ -61,6 +62,7 @@ abbrev TrailingParserDescr := ParserDescrCore ParserKind.trailing
 @[matchPattern] abbrev ParserDescr.sepBy1 := @ParserDescrCore.sepBy1
 @[matchPattern] abbrev ParserDescr.node := @ParserDescrCore.node
 @[matchPattern] abbrev ParserDescr.symbol := @ParserDescrCore.symbol
+@[matchPattern] abbrev ParserDescr.tacticSymbol := @ParserDescrCore.tacticSymbol
 @[matchPattern] abbrev ParserDescr.unicodeSymbol := @ParserDescrCore.unicodeSymbol
 @[matchPattern] abbrev ParserDescr.pushLeading := @ParserDescrCore.pushLeading
 @[matchPattern] abbrev ParserDescr.parser := @ParserDescrCore.parser

stage0/stdlib/Init/Lean/Elab.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Elab
-// Imports: Init.Lean.Elab.Import Init.Lean.Elab.Exception Init.Lean.Elab.ElabStrategyAttrs Init.Lean.Elab.Command Init.Lean.Elab.Term Init.Lean.Elab.TermApp Init.Lean.Elab.TermBinders Init.Lean.Elab.Quotation Init.Lean.Elab.Frontend Init.Lean.Elab.BuiltinNotation Init.Lean.Elab.Declaration
+// Imports: Init.Lean.Elab.Import Init.Lean.Elab.Exception Init.Lean.Elab.ElabStrategyAttrs Init.Lean.Elab.Command Init.Lean.Elab.Term Init.Lean.Elab.TermApp Init.Lean.Elab.TermBinders Init.Lean.Elab.Quotation Init.Lean.Elab.Frontend Init.Lean.Elab.BuiltinNotation Init.Lean.Elab.Declaration Init.Lean.Elab.Tactic
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -24,6 +24,7 @@ lean_object* initialize_Init_Lean_Elab_Quotation(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Frontend(lean_object*);
 lean_object* initialize_Init_Lean_Elab_BuiltinNotation(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Declaration(lean_object*);
+lean_object* initialize_Init_Lean_Elab_Tactic(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean_Elab(lean_object* w) {
 lean_object * res;
@@ -62,6 +63,9 @@ lean_dec_ref(res);
 res = initialize_Init_Lean_Elab_Declaration(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Elab_Tactic(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus

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

@@ -0,0 +1,147 @@
+// Lean compiler output
+// Module: Init.Lean.Elab.Tactic
+// Imports: Init.Lean.Elab.Term
+#include "runtime/lean.h"
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock(lean_object*);
+extern lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__2;
+lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__3;
+lean_object* l_Lean_Elab_Term_elabTacticBlock___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_elabTacticBlock___closed__1;
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_elabTacticBlock___closed__2;
+lean_object* l_Lean_Elab_Term_elabTacticBlock___closed__3;
+extern lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__4;
+lean_object* l_Lean_Elab_Term_addBuiltinTermElab(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__2;
+lean_object* l_Lean_Elab_Term_elabTacticBlock(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__1;
+lean_object* _init_l_Lean_Elab_Term_elabTacticBlock___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("not implemented yet ");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Elab_Term_elabTacticBlock___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Elab_Term_elabTacticBlock___closed__1;
+x_2 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_Elab_Term_elabTacticBlock___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Elab_Term_elabTacticBlock___closed__2;
+x_2 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+lean_object* l_Lean_Elab_Term_elabTacticBlock(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_inc(x_1);
+x_5 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_5, 0, x_1);
+x_6 = l_Lean_Elab_Term_elabTacticBlock___closed__3;
+x_7 = lean_alloc_ctor(8, 2, 0);
+lean_ctor_set(x_7, 0, x_6);
+lean_ctor_set(x_7, 1, x_5);
+x_8 = l_Lean_Elab_Term_throwError___rarg(x_1, x_7, x_3, x_4);
+return x_8;
+}
+}
+lean_object* l_Lean_Elab_Term_elabTacticBlock___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_elabTacticBlock(x_1, x_2, x_3, x_4);
+lean_dec(x_2);
+return x_5;
+}
+}
+lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("elabTacticBlock");
+return x_1;
+}
+}
+lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___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_elabTacticBlock___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__3() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabTacticBlock___boxed), 4, 0);
+return x_1;
+}
+}
+lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock(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_tacticBlock___elambda__1___closed__2;
+x_3 = l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__2;
+x_4 = l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__3;
+x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
+lean_object* initialize_Init_Lean_Elab_Term(lean_object*);
+static bool _G_initialized = false;
+lean_object* initialize_Init_Lean_Elab_Tactic(lean_object* w) {
+lean_object * res;
+if (_G_initialized) return lean_mk_io_result(lean_box(0));
+_G_initialized = true;
+res = initialize_Init_Lean_Elab_Term(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_Lean_Elab_Term_elabTacticBlock___closed__1 = _init_l_Lean_Elab_Term_elabTacticBlock___closed__1();
+lean_mark_persistent(l_Lean_Elab_Term_elabTacticBlock___closed__1);
+l_Lean_Elab_Term_elabTacticBlock___closed__2 = _init_l_Lean_Elab_Term_elabTacticBlock___closed__2();
+lean_mark_persistent(l_Lean_Elab_Term_elabTacticBlock___closed__2);
+l_Lean_Elab_Term_elabTacticBlock___closed__3 = _init_l_Lean_Elab_Term_elabTacticBlock___closed__3();
+lean_mark_persistent(l_Lean_Elab_Term_elabTacticBlock___closed__3);
+l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__1();
+lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__1);
+l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__2();
+lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__2);
+l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__3();
+lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__3);
+res = l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+return lean_mk_io_result(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif

stage0/stdlib/Init/Lean/Parser/Tactic.c

@@ -20,17 +20,14 @@ extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Tactic_orelse___closed__2;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__15;
 lean_object* l_Lean_Parser_Tactic_intros___closed__7;
-lean_object* l_Lean_Parser_Tactic_tacticSymbolInfo___elambda__2(lean_object*);
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__1;
 extern lean_object* l_Lean_Parser_declareLeadingBuiltinParser___closed__1;
 lean_object* l_Lean_Parser_andthenInfo(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_have___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Tactic_apply___closed__2;
 lean_object* l_Lean_Parser_regBuiltinTacticParserAttr___closed__1;
-lean_object* l_Lean_Parser_Tactic_tacticSymbolInfo___elambda__1(lean_object*);
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__14;
 lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__5;
-lean_object* l_Lean_Parser_Tactic_tacticSymbolInfo___closed__1;
 extern lean_object* l_Lean_nullKind;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___closed__2;
 lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__3;
@@ -47,7 +44,6 @@ lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__4;
 extern lean_object* l_Lean_Parser_Term_have___closed__3;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly;
 extern lean_object* l_Lean_Parser_Term_subtype___closed__1;
-lean_object* l_Lean_Parser_Tactic_tacticSymbolInfo___closed__2;
 lean_object* l_Lean_Parser_tacticSeq___closed__2;
 lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_apply___closed__4;
@@ -78,7 +74,6 @@ lean_object* l_Lean_Parser_Tactic_apply___closed__5;
 lean_object* l_Lean_Parser_Tactic_assumption___closed__4;
 lean_object* l_Lean_Parser_Tactic_intros___closed__6;
 lean_object* l_Lean_Parser_tacticParser(uint8_t, lean_object*);
-lean_object* l_Lean_Parser_Tactic_tacticSymbol(uint8_t, lean_object*);
 lean_object* l_Lean_Parser_regBuiltinTacticParserAttr___closed__2;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__13;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__11;
@@ -147,8 +142,8 @@ lean_object* l_Lean_Parser_tacticSeq(uint8_t);
 lean_object* l_Lean_Parser_Tactic_intros___closed__4;
 lean_object* l_Lean_Parser_sepBy1Info(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__5;
+lean_object* l_Lean_Parser_tacticSymbolInfo(lean_object*);
 extern lean_object* l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
-lean_object* l_Lean_Parser_nonReservedSymbol___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___closed__2;
 lean_object* l_Lean_Parser_Tactic_assumption___elambda__1___closed__1;
@@ -156,7 +151,6 @@ lean_object* l_Lean_Parser_mergeOrElseErrors(lean_object*, lean_object*, lean_ob
 lean_object* l_Lean_Parser_categoryParser(uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__4;
 lean_object* l_Lean_Parser_regTacticParserAttribute(lean_object*);
-lean_object* l_Lean_Parser_Tactic_tacticSymbolInfo___elambda__1___boxed(lean_object*);
 lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__6;
 lean_object* l_Lean_Parser_sepBy1Fn(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -175,7 +169,6 @@ lean_object* l_Lean_Parser_Tactic_intro___closed__6;
 lean_object* l_Lean_Parser_Tactic_intros;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___closed__5;
-lean_object* l_Lean_Parser_Tactic_tacticSymbolInfo(lean_object*);
 lean_object* l_String_trim(lean_object*);
 lean_object* l_Lean_Parser_Tactic_apply___closed__1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_assumption(lean_object*);
@@ -188,7 +181,6 @@ lean_object* l_Lean_Parser_regBuiltinTacticParserAttr___closed__3;
 lean_object* l_Lean_Parser_mkAntiquot(uint8_t, lean_object*, lean_object*, uint8_t);
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___closed__5;
 lean_object* l_Lean_Parser_Tactic_assumption___elambda__1___closed__7;
-lean_object* l_Lean_Parser_Tactic_tacticSymbolInfo___elambda__2___boxed(lean_object*);
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___closed__3;
 lean_object* l_Lean_Parser_Tactic_intro___closed__1;
 lean_object* l_Lean_Parser_Tactic_intro___closed__3;
@@ -201,7 +193,6 @@ lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Tactic_assumption___elambda__1(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Parser_Tactic_tacticSymbol___boxed(lean_object*, lean_object*);
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_orelse(lean_object*);
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_categoryParser___elambda__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -258,7 +249,7 @@ _start:
 lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; 
 x_2 = l_Lean_Parser_regBuiltinTacticParserAttr___closed__2;
 x_3 = l_Lean_Parser_regBuiltinTacticParserAttr___closed__4;
-x_4 = 0;
+x_4 = 1;
 x_5 = l_Lean_Parser_registerBuiltinParserAttribute(x_2, x_3, x_4, x_1);
 return x_5;
 }
@@ -386,104 +377,6 @@ x_3 = l_Lean_Parser_tacticSeq(x_2);
 return x_3;
 }
 }
-lean_object* l_Lean_Parser_Tactic_tacticSymbolInfo___elambda__1(lean_object* x_1) {
-_start:
-{
-lean_inc(x_1);
-return x_1;
-}
-}
-lean_object* l_Lean_Parser_Tactic_tacticSymbolInfo___elambda__2(lean_object* x_1) {
-_start:
-{
-lean_inc(x_1);
-return x_1;
-}
-}
-lean_object* _init_l_Lean_Parser_Tactic_tacticSymbolInfo___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_tacticSymbolInfo___elambda__2___boxed), 1, 0);
-return x_1;
-}
-}
-lean_object* _init_l_Lean_Parser_Tactic_tacticSymbolInfo___closed__2() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_tacticSymbolInfo___elambda__1___boxed), 1, 0);
-return x_1;
-}
-}
-lean_object* l_Lean_Parser_Tactic_tacticSymbolInfo(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
-x_2 = lean_box(0);
-x_3 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_3, 0, x_1);
-lean_ctor_set(x_3, 1, x_2);
-lean_ctor_set(x_3, 2, x_2);
-x_4 = lean_box(0);
-x_5 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_5, 0, x_3);
-lean_ctor_set(x_5, 1, x_4);
-x_6 = lean_alloc_ctor(2, 1, 0);
-lean_ctor_set(x_6, 0, x_5);
-x_7 = l_Lean_Parser_Tactic_tacticSymbolInfo___closed__1;
-x_8 = l_Lean_Parser_Tactic_tacticSymbolInfo___closed__2;
-x_9 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_9, 0, x_7);
-lean_ctor_set(x_9, 1, x_8);
-lean_ctor_set(x_9, 2, x_6);
-return x_9;
-}
-}
-lean_object* l_Lean_Parser_Tactic_tacticSymbolInfo___elambda__1___boxed(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = l_Lean_Parser_Tactic_tacticSymbolInfo___elambda__1(x_1);
-lean_dec(x_1);
-return x_2;
-}
-}
-lean_object* l_Lean_Parser_Tactic_tacticSymbolInfo___elambda__2___boxed(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = l_Lean_Parser_Tactic_tacticSymbolInfo___elambda__2(x_1);
-lean_dec(x_1);
-return x_2;
-}
-}
-lean_object* l_Lean_Parser_Tactic_tacticSymbol(uint8_t x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_3 = l_String_trim(x_2);
-lean_inc(x_3);
-x_4 = l_Lean_Parser_Tactic_tacticSymbolInfo(x_3);
-x_5 = lean_alloc_closure((void*)(l_Lean_Parser_nonReservedSymbol___lambda__1___boxed), 4, 1);
-lean_closure_set(x_5, 0, x_3);
-x_6 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_6, 0, x_4);
-lean_ctor_set(x_6, 1, x_5);
-return x_6;
-}
-}
-lean_object* l_Lean_Parser_Tactic_tacticSymbol___boxed(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-uint8_t x_3; lean_object* x_4; 
-x_3 = lean_unbox(x_1);
-lean_dec(x_1);
-x_4 = l_Lean_Parser_Tactic_tacticSymbol(x_3, x_2);
-lean_dec(x_2);
-return x_4;
-}
-}
 lean_object* _init_l_Lean_Parser_Tactic_intro___elambda__1___closed__1() {
 _start:
 {
@@ -725,7 +618,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; 
 x_1 = l_Lean_Parser_Tactic_intro___elambda__1___closed__8;
-x_2 = l_Lean_Parser_Tactic_tacticSymbolInfo(x_1);
+x_2 = l_Lean_Parser_tacticSymbolInfo(x_1);
 return x_2;
 }
 }
@@ -994,7 +887,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; 
 x_1 = l_Lean_Parser_Tactic_intros___elambda__1___closed__6;
-x_2 = l_Lean_Parser_Tactic_tacticSymbolInfo(x_1);
+x_2 = l_Lean_Parser_tacticSymbolInfo(x_1);
 return x_2;
 }
 }
@@ -1219,7 +1112,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; 
 x_1 = l_Lean_Parser_Tactic_assumption___elambda__1___closed__5;
-x_2 = l_Lean_Parser_Tactic_tacticSymbolInfo(x_1);
+x_2 = l_Lean_Parser_tacticSymbolInfo(x_1);
 return x_2;
 }
 }
@@ -1452,7 +1345,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; 
 x_1 = l_Lean_Parser_Tactic_apply___elambda__1___closed__6;
-x_2 = l_Lean_Parser_Tactic_tacticSymbolInfo(x_1);
+x_2 = l_Lean_Parser_tacticSymbolInfo(x_1);
 return x_2;
 }
 }
@@ -2827,10 +2720,6 @@ l_Lean_Parser_tacticSeq___closed__1 = _init_l_Lean_Parser_tacticSeq___closed__1(
 lean_mark_persistent(l_Lean_Parser_tacticSeq___closed__1);
 l_Lean_Parser_tacticSeq___closed__2 = _init_l_Lean_Parser_tacticSeq___closed__2();
 lean_mark_persistent(l_Lean_Parser_tacticSeq___closed__2);
-l_Lean_Parser_Tactic_tacticSymbolInfo___closed__1 = _init_l_Lean_Parser_Tactic_tacticSymbolInfo___closed__1();
-lean_mark_persistent(l_Lean_Parser_Tactic_tacticSymbolInfo___closed__1);
-l_Lean_Parser_Tactic_tacticSymbolInfo___closed__2 = _init_l_Lean_Parser_Tactic_tacticSymbolInfo___closed__2();
-lean_mark_persistent(l_Lean_Parser_Tactic_tacticSymbolInfo___closed__2);
 l_Lean_Parser_Tactic_intro___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_intro___elambda__1___closed__1();
 lean_mark_persistent(l_Lean_Parser_Tactic_intro___elambda__1___closed__1);
 l_Lean_Parser_Tactic_intro___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_intro___elambda__1___closed__2();

stage0/stdlib/Init/LeanExt.c

@@ -23,6 +23,7 @@ extern lean_object* l_String_splitAux___main___closed__1;
 lean_object* l_Lean_ParserDescr_try(uint8_t, lean_object*);
 lean_object* l_Lean_ParserDescr_unicodeSymbol(uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescrCore_inhabited(uint8_t);
+lean_object* l_Lean_ParserDescr_tacticSymbol(lean_object*);
 lean_object* l_Lean_ParserDescr_many1(uint8_t, lean_object*);
 lean_object* l_Lean_ParserDescr_many___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_many1___boxed(lean_object*, lean_object*);
@@ -291,6 +292,15 @@ x_5 = l_Lean_ParserDescr_symbol(x_4, x_2, x_3);
 return x_5;
 }
 }
+lean_object* l_Lean_ParserDescr_tacticSymbol(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_ctor(12, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
 lean_object* l_Lean_ParserDescr_unicodeSymbol(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
@@ -317,7 +327,7 @@ lean_object* _init_l_Lean_ParserDescr_pushLeading() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_box(12);
+x_1 = lean_box(13);
 return x_1;
 }
 }
@@ -325,7 +335,7 @@ lean_object* l_Lean_ParserDescr_parser(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_alloc_ctor(13, 2, 0);
+x_3 = lean_alloc_ctor(14, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
 return x_3;