diff --git a/src/Init.lean b/src/Init.lean index b636f37730..54741d4ed8 100644 --- 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 deleted file mode 100644 index 3561280e8d..0000000000 --- a/src/Init/Enum.lean +++ /dev/null @@ -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) diff --git a/tests/lean/run/654.lean b/tests/lean/run/654.lean index 53bf14659d..78385ab443 100644 --- a/tests/lean/run/654.lean +++ b/tests/lean/run/654.lean @@ -1,4 +1,4 @@ -enum Foo where +inductive Foo where | a | b | c def f : Foo → Nat @@ -6,9 +6,7 @@ def f : Foo → Nat | 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