From 27e26998d2d2c3e39d75439867cb426496b17da4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 20 Nov 2020 13:57:52 -0800 Subject: [PATCH] chore: prepare to change `structInst` syntax --- src/Lean/Parser/Term.lean | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 2af25e26a1..03194d5f4a 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -70,7 +70,16 @@ def sufficesDecl := optIdent >> termParser >> (fromTerm <|> byTactic) def structInstArrayRef := parser! "[" >> termParser >>"]" def structInstLVal := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef) def structInstField := ppGroup $ parser! structInstLVal >> " := " >> termParser -@[builtinTermParser] def structInst := parser! "{" >> ppHardSpace >> optional (atomic (termParser >> " with ")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> " }" +@[builtinTermParser] def structInst := parser! + (checkInsideQuot >> + "{" >> ppHardSpace >> optional (atomic (termParser >> " with ")) + >> manyIndent (group (structInstField >> optional ", ")) + >> optional ".." + >> optional (" : " >> termParser) >> " }") + <|> + (checkOutsideQuot >> + "{" >> ppHardSpace >> optional (atomic (termParser >> " with ")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> " }") + def typeSpec := parser! " : " >> termParser def optType : Parser := optional typeSpec @[builtinTermParser] def explicit := parser! "@" >> termParser maxPrec