chore: update stage0

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

@@ -7,3 +7,4 @@ prelude
 import Init.Lean.Elab.Term
 import Init.Lean.Elab.Tactic.Basic
 import Init.Lean.Elab.Tactic.ElabTerm
+import Init.Lean.Elab.Tactic.Induction

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

@@ -0,0 +1,19 @@
+/-
+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.Tactic.Basic
+
+namespace Lean
+namespace Elab
+namespace Tactic
+
+@[builtinTactic «induction»] def evalInduction : Tactic :=
+fun stx => focus stx $
+  throwError stx ("WIP " ++ stx)
+
+end Tactic
+end Elab
+end Lean

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

@@ -36,6 +36,7 @@ def ident' : Parser := ident <|> underscore
 @[builtinTacticParser] def «allGoals»   := parser! nonReservedSymbol "allGoals " >> tacticParser
 @[builtinTacticParser] def «skip»       := parser! nonReservedSymbol "skip"
 @[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
+@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize" >> optional (try (ident >> " : ")) >> termParser 50 >> " = " >> ident
 def majorPremise := parser! optional (try (ident >> " : ")) >> termParser
 def inductionAlt  : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident >> many ident >> darrow >> termParser
 def inductionAlts : Parser := withPosition $ fun pos => "|" >> sepBy1 inductionAlt (checkColGe pos.column "alternatives must be indented" >> "|")

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

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Elab.Tactic
-// Imports: Init.Lean.Elab.Term Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.Tactic.ElabTerm
+// Imports: Init.Lean.Elab.Term Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.Tactic.ElabTerm Init.Lean.Elab.Tactic.Induction
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -16,6 +16,7 @@ extern "C" {
 lean_object* initialize_Init_Lean_Elab_Term(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Tactic_Basic(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Tactic_ElabTerm(lean_object*);
+lean_object* initialize_Init_Lean_Elab_Tactic_Induction(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean_Elab_Tactic(lean_object* w) {
 lean_object * res;
@@ -30,6 +31,9 @@ lean_dec_ref(res);
 res = initialize_Init_Lean_Elab_Tactic_ElabTerm(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Elab_Tactic_Induction(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/Induction.c

@@ -0,0 +1,142 @@
+// Lean compiler output
+// Module: Init.Lean.Elab.Tactic.Induction
+// Imports: Init.Lean.Elab.Tactic.Basic
+#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_Lean_Elab_Tactic_evalInduction___closed__1;
+lean_object* l_Lean_Elab_Tactic_evalInduction___closed__2;
+extern lean_object* l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3;
+lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__3;
+lean_object* l_Lean_Elab_Tactic_focus___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__2;
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
+lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__1;
+lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction(lean_object*);
+lean_object* l_Lean_Elab_Tactic_evalInduction___closed__3;
+extern lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__2;
+lean_object* l_Lean_Elab_Tactic_evalInduction(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_addBuiltinTactic(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* _init_l_Lean_Elab_Tactic_evalInduction___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("WIP ");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Elab_Tactic_evalInduction___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Elab_Tactic_evalInduction___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_Tactic_evalInduction___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Elab_Tactic_evalInduction___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_Tactic_evalInduction(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; 
+lean_inc(x_1);
+x_4 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_4, 0, x_1);
+x_5 = l_Lean_Elab_Tactic_evalInduction___closed__3;
+x_6 = lean_alloc_ctor(9, 2, 0);
+lean_ctor_set(x_6, 0, x_5);
+lean_ctor_set(x_6, 1, x_4);
+lean_inc(x_1);
+x_7 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_throwError___rarg), 4, 2);
+lean_closure_set(x_7, 0, x_1);
+lean_closure_set(x_7, 1, x_6);
+x_8 = l_Lean_Elab_Tactic_focus___rarg(x_1, x_7, x_2, x_3);
+return x_8;
+}
+}
+lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("evalInduction");
+return x_1;
+}
+}
+lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3;
+x_2 = l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__3() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInduction), 3, 0);
+return x_1;
+}
+}
+lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction(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_Tactic_induction___elambda__1___closed__2;
+x_3 = l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__2;
+x_4 = l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__3;
+x_5 = l_Lean_Elab_Tactic_addBuiltinTactic(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
+lean_object* initialize_Init_Lean_Elab_Tactic_Basic(lean_object*);
+static bool _G_initialized = false;
+lean_object* initialize_Init_Lean_Elab_Tactic_Induction(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_Tactic_Basic(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_Lean_Elab_Tactic_evalInduction___closed__1 = _init_l_Lean_Elab_Tactic_evalInduction___closed__1();
+lean_mark_persistent(l_Lean_Elab_Tactic_evalInduction___closed__1);
+l_Lean_Elab_Tactic_evalInduction___closed__2 = _init_l_Lean_Elab_Tactic_evalInduction___closed__2();
+lean_mark_persistent(l_Lean_Elab_Tactic_evalInduction___closed__2);
+l_Lean_Elab_Tactic_evalInduction___closed__3 = _init_l_Lean_Elab_Tactic_evalInduction___closed__3();
+lean_mark_persistent(l_Lean_Elab_Tactic_evalInduction___closed__3);
+l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__1 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__1();
+lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__1);
+l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__2 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__2();
+lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__2);
+l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__3 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__3();
+lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__3);
+res = l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction(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