From cdb7e0cfae9d02b090708f41efd87a01571a9118 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 2 Feb 2020 17:30:36 -0800 Subject: [PATCH] feat: add `structInstLVal` --- src/Init/Lean/Parser/Term.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean index 8f99ca8c32..35b79e94c2 100644 --- a/src/Init/Lean/Parser/Term.lean +++ b/src/Init/Lean/Parser/Term.lean @@ -58,7 +58,9 @@ def haveAssign := parser! " := " >> termParser @[builtinTermParser] def «suffices» := parser! "suffices " >> optIdent >> termParser >> fromTerm >> "; " >> termParser @[builtinTermParser] def «show» := parser! "show " >> termParser >> fromTerm @[builtinTermParser] def «fun» := parser! unicodeSymbol "λ" "fun" >> many1 (termParser appPrec) >> darrow >> termParser -def structInstField := parser! ident >> " := " >> termParser +def structInstArrayRef := parser! symbol "[" (appPrec+1) >> termParser >>"]" +def structInstLVal := (ident <|> structInstArrayRef) >> many (("." >> ident) <|> structInstArrayRef) +def structInstField := parser! structInstLVal >> " := " >> termParser def structInstSource := parser! ".." >> optional termParser @[builtinTermParser] def structInst := parser! symbol "{" appPrec >> optional (try (ident >> " . ")) >> sepBy (structInstField <|> structInstSource) ", " true >> "}" def typeSpec := parser! " : " >> termParser