max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/parser/term): allow type annotation after pattern

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-16 13:21:02 -07:00
parent 86d7904ea7
commit e59edb27cd
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/parser/term.lean
View file

@ -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 " ← " " <- "