chore: remove enum command

Now, `inductive` is also efficient for big enumeration types
leanprover · Sep 6, 2021 · 70f2200 · 70f2200
1 parent 1ce2ff3
commit 70f2200
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 42 deletions.
diff --git a/src/Init.lean b/src/Init.lean
@@ -19,4 +19,3 @@ import Init.NotationExtra
 import Init.SimpLemmas
 import Init.Hints
 import Init.Conv
-import Init.Enum
diff --git a/src/Init/Enum.lean b/src/Init/Enum.lean
diff --git a/tests/lean/run/654.lean b/tests/lean/run/654.lean
@@ -1,14 +1,12 @@
-enum Foo where
+inductive Foo where
   | a | b | c
 
 def f : Foo → Nat
   | Foo.a => 10
   | Foo.b => 20
   | Foo.c => 35
 
-#eval Foo.b
-
-enum CXCursorKind where
+inductive CXCursorKind where
   | CXCursor_UnexposedDecl
   | CXCursor_StructDecl
   | CXCursor_UnionDecl
@@ -285,5 +283,3 @@ open CXCursorKind
 
 example (h : CXCursor_CUDAGlobalAttr = CXCursor_CUDAHostAttr) : False := by
   contradiction
-
-#eval CXCursor_CUDAConstantAttr