From f427a6bd3f8da74152bdff1f8d148b9a1fc4b207 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 20 May 2020 16:57:58 -0700
Subject: [PATCH] feat: new structure instance syntax

---
 src/Init/Lean/Parser/Term.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean
index 3e0f5593ae..aa6f64dec1 100644
--- a/src/Init/Lean/Parser/Term.lean
+++ b/src/Init/Lean/Parser/Term.lean
@@ -75,8 +75,7 @@ def haveAssign := parser! " := " >> termParser
 def structInstArrayRef := parser! "[" >> termParser >>"]"
 def structInstLVal   := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
 def structInstField  := parser! structInstLVal >> " := " >> termParser
-def structInstSource := parser! ".." >> optional termParser
-@[builtinTermParser] def structInst := parser! symbol "{" appPrec >> optional (try (ident >> checkWsBefore "expected space '.'" >> " . ")) >> sepBy (structInstField <|> structInstSource) ", " true >> "}"
+@[builtinTermParser] def structInst := parser! symbol "{" appPrec >> optional (try (termParser >> "with")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> "}"
 def typeSpec := parser! " : " >> termParser
 def optType : Parser := optional typeSpec
 @[builtinTermParser] def subtype := parser! "{" >> ident >> optType >> " // " >> termParser >> "}"