From 7af9de41cab2bc628add464b7931bb0a82bb9b44 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 15 Jul 2019 14:12:13 -0700 Subject: [PATCH] feat(library/init/lean/parser/term): add `borrowed` syntax --- library/init/lean/parser/term.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index 7fcd6679d3..7eb5d63549 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -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