From 69d8809ff5db9cd080ac67de69b302f58fb60de5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Feb 2020 14:32:11 -0800 Subject: [PATCH] chore: allow `numLit` --- src/Init/Lean/Parser/Term.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean index 36f255580a..5738e12bb6 100644 --- a/src/Init/Lean/Parser/Term.lean +++ b/src/Init/Lean/Parser/Term.lean @@ -61,7 +61,7 @@ def haveAssign := parser! " := " >> termParser @[builtinTermParser] def «show» := parser! symbol "show " leadPrec >> termParser >> fromTerm @[builtinTermParser] def «fun» := parser! unicodeSymbol "λ" "fun" leadPrec >> many1 (termParser appPrec) >> darrow >> termParser def structInstArrayRef := parser! "[" >> termParser >>"]" -def structInstLVal := (ident <|> structInstArrayRef) >> many (group ("." >> (ident <|> numLit)) <|> structInstArrayRef) +def structInstLVal := (ident <|> numLit <|> structInstArrayRef) >> many (group ("." >> (ident <|> numLit)) <|> structInstArrayRef) def structInstField := parser! structInstLVal >> " := " >> termParser def structInstSource := parser! ".." >> optional termParser @[builtinTermParser] def structInst := parser! symbol "{" appPrec >> optional (try (ident >> " . ")) >> sepBy (structInstField <|> structInstSource) ", " true >> "}"