From 58b21fe0c96d8b5e3ca2e747ffe4a249d3997ffa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Jan 2020 19:41:40 -0800 Subject: [PATCH] feat: mark literals as valid kinds --- src/Init/Lean/Parser/Parser.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index 56ed84147d..f9b269ec91 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -1667,7 +1667,7 @@ parserExtension.addEntry env $ ParserExtensionEntry.kind k def isValidSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Bool := let kinds := (parserExtension.getState env).kinds; -kinds.contains k || k == `choice +kinds.contains k || k == choiceKind || k == strLitKind || k == numLitKind || k == charLitKind def getSyntaxNodeKinds (env : Environment) : List SyntaxNodeKind := do let kinds := (parserExtension.getState env).kinds;