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

feat(library/init/lean/parser/term): add borrowed syntax

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-15 14:12:13 -07:00
parent 299c3a0791
commit 7af9de41ca
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -89,6 +89,7 @@ def matchAlt := parser! " | " >> sepBy1 termParser ", " >> " => " >> termParser
@[builtinTermParser] def «nomatch» := parser! "nomatch " >> termParser
@[builtinTermParser] def «parser!» := parser! "parser! " >> termParser
@[builtinTermParser] def «tparser!» := parser! "tparser! " >> termParser
@[builtinTermParser] def borrowed := parser! symbol "@&" appPrec >> termParser (appPrec - 1)
/- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/
def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders" >> many bracktedBinder >> optType