chore: update stage0

stage0/src/Init.lean

@@ -19,4 +19,3 @@ import Init.NotationExtra
 import Init.SimpLemmas
 import Init.Hints
 import Init.Conv
-import Init.Enum

stage0/src/Init/Enum.lean

@@ -1,35 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.NotationExtra
-import Init.Data.Range
-import Init.Data.Stream
-
-/--
-  Macro for declaring big enumeration types. It is more efficient than using `inductive`.
-
-  It also generates the instances `BEq`, `DecidableEq`, `Inhabited`, and `Repr` for the new type
--/
-macro "enum " n:ident " where " cs:(group("| " ident))+ : command => open Lean in do
-  let cs := cs.getArgs
-  let numCtors := cs.size
-  let structDecl ← `(structure $n:ident where (val : Fin $(quote numCtors)))
-  let derivingCmd ← `(deriving instance BEq, DecidableEq, Inhabited for $n:ident)
-  let currNamespace ← Macro.getCurrNamespace
-  let mkCtorName (ctorDeclStx : Syntax) : Name :=
-    n.getId ++ ctorDeclStx[1].getId
-  let mut ctorDefs := #[]
-  for c in cs, i in [:numCtors] do
-    let ctorName := mkCtorName c
-    let ctorDef ← `(@[matchPattern] abbrev $(mkIdentFrom c ctorName):ident : $n:ident := ⟨$(quote i)⟩)
-    ctorDefs := ctorDefs.push ctorDef
-  -- generate `Repr` instance
-  let ctorFmts ← cs.mapM fun c =>
-    `(Std.format $(quote <| toString (currNamespace ++ mkCtorName c)))
-  let reprInst ← `(
-    def enumFmts : Array Std.Format := [ $(ctorFmts),*].toArray
-    instance : Repr $n := ⟨fun e _ => enumFmts[e.val.val]⟩)
-  return mkNullNode (#[structDecl, derivingCmd, reprInst] ++ ctorDefs)

stage0/stdlib/Init.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init
-// Imports: Init.Prelude Init.Notation Init.Core Init.Control Init.Data.Basic Init.WF Init.Data Init.System Init.Util Init.Fix Init.Meta Init.NotationExtra Init.SimpLemmas Init.Hints Init.Conv Init.Enum
+// Imports: Init.Prelude Init.Notation Init.Core Init.Control Init.Data.Basic Init.WF Init.Data Init.System Init.Util Init.Fix Init.Meta Init.NotationExtra Init.SimpLemmas Init.Hints Init.Conv
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -28,7 +28,6 @@ lean_object* initialize_Init_NotationExtra(lean_object*);
 lean_object* initialize_Init_SimpLemmas(lean_object*);
 lean_object* initialize_Init_Hints(lean_object*);
 lean_object* initialize_Init_Conv(lean_object*);
-lean_object* initialize_Init_Enum(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init(lean_object* w) {
 lean_object * res;
@@ -79,9 +78,6 @@ lean_dec_ref(res);
 res = initialize_Init_Conv(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = initialize_Init_Enum(lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus