From e59edb27cdae31c3a56cfad5166289c18b8bb20d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Jul 2019 13:21:02 -0700
Subject: [PATCH] feat(library/init/lean/parser/term): allow type annotation
 after pattern

---
 library/init/lean/parser/term.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index fb98131a3c..8f63976c4e 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -100,7 +100,7 @@ def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders"
 def letIdDecl         := parser! try (letIdLhs >> " := ") >> termParser
 def equation := parser! " | " >> many1 (termParser appPrec) >> " := " >> termParser
 def letEqns           := parser! try (letIdLhs >> lookahead " | ") >> many1Indent equation "equations must be indented"
-def letPatDecl        := parser! termParser >> " := " >> termParser
+def letPatDecl        := parser! termParser >> optType >> " := " >> termParser
 def letDecl           := try letIdDecl <|> letEqns <|> letPatDecl
 @[builtinTermParser] def «let» := parser! "let " >> letDecl >> "; " >> termParser
 def leftArrow : Parser := unicodeSymbol " ← " " <- "