From 5eebbc7bdadfa0ba853e9de8055a4e68f9aaa0d2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Jan 2020 14:34:30 -0800 Subject: [PATCH] chore: remove unnecessary attributes If one day we add elaboration functions for level and syntax, then we can add them back. --- src/Init/Lean/Parser/Level.lean | 3 --- src/Init/Lean/Parser/Syntax.lean | 3 --- 2 files changed, 6 deletions(-) diff --git a/src/Init/Lean/Parser/Level.lean b/src/Init/Lean/Parser/Level.lean index 4b1ab733d9..76fb69d744 100644 --- a/src/Init/Lean/Parser/Level.lean +++ b/src/Init/Lean/Parser/Level.lean @@ -12,9 +12,6 @@ namespace Parser @[init] def regBuiltinLevelParserAttr : IO Unit := registerBuiltinParserAttribute `builtinLevelParser `level -@[init] def regLevelParserAttribute : IO Unit := -registerBuiltinDynamicParserAttribute `levelParser `level - @[inline] def levelParser {k : ParserKind} (rbp : Nat := 0) : Parser k := categoryParser `level rbp diff --git a/src/Init/Lean/Parser/Syntax.lean b/src/Init/Lean/Parser/Syntax.lean index f2744774d3..156d28a1a1 100644 --- a/src/Init/Lean/Parser/Syntax.lean +++ b/src/Init/Lean/Parser/Syntax.lean @@ -13,9 +13,6 @@ namespace Parser let leadingIdentAsSymbol := true; registerBuiltinParserAttribute `builtinSyntaxParser `syntax leadingIdentAsSymbol -@[init] def regSyntaxParserAttribute : IO Unit := -registerBuiltinDynamicParserAttribute `syntaxParser `syntax - @[inline] def syntaxParser {k : ParserKind} (rbp : Nat := 0) : Parser k := categoryParser `syntax rbp