max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: mark literals as valid kinds

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-18 19:41:40 -08:00
parent be571e8d42
commit 58b21fe0c9
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Parser/Parser.lean
View file

@ -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;