From 68d29fcdd4b19e7c9652f975f7896048a652cd98 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 5 Jul 2019 12:09:59 -0700
Subject: [PATCH] feat(library/init/lean/parser/term): structure instances and
 subtypes

---
 library/init/lean/parser/term.lean | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 709eaff2b5..2e2b071860 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -32,15 +32,21 @@ namespace Term
 @[builtinTermParser] def paren := parser! symbol "(" maxPrec >> optional (termParser >> parenSpecial) >> ")"
 @[builtinTermParser] def anonymousCtor := parser! symbol "⟨" maxPrec >> sepBy1 termParser ", " >> symbol "⟩"
 @[inline] def optIdent : Parser := optional (try (ident >> " : "))
-@[builtinTermParser] def ifTerm    := parser! "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
+@[builtinTermParser] def «if»  := parser! "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
 def fromTerm   := parser! " from " >> termParser
 def haveAssign := parser! " := " >> termParser
-@[builtinTermParser] def haveTerm     := parser! "have " >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> termParser
-@[builtinTermParser] def sufficesTerm := parser! "suffices " >> optIdent >> termParser >> fromTerm >> "; " >> termParser
-@[builtinTermParser] def showTerm     := parser! "show " >> termParser >> fromTerm
-@[builtinTermParser] def funTerm      := parser! unicodeSymbol "λ" "fun" >> many1 (termParser maxPrec) >> unicodeSymbol "⇒" "=>" >> termParser
+@[builtinTermParser] def «have» := parser! "have " >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> 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 maxPrec) >> unicodeSymbol "⇒" "=>" >> termParser
+def structInstField  := parser! ident >> " := " >> termParser
+def structInstSource := parser! ".." -- >> optional termParser
+@[builtinTermParser] def structInst := parser! symbol "{" maxPrec >> optional (try (ident >> " . ")) >> sepBy (structInstField <|> structInstSource) ", " true >> "}"
+def typeSpec := parser! " : " >> termParser
+def optType : Parser := optional typeSpec
+@[builtinTermParser] def subtype := parser! "{" >> ident >> optType >> " // " >> termParser >> "}"
 
-@[builtinTermParser] def appTerm := tparser! pushLeading >> termParser maxPrec
+@[builtinTermParser] def app := tparser! pushLeading >> termParser maxPrec
 
 end Term