From abf78e162c0450fb02f27d124acf5cbeaff3e8e9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 12 Apr 2021 22:33:23 -0700 Subject: [PATCH] feat: add notation for disabling implicit lambda feature This notation will be useful for writing macros where implicit lambdas are not desired. --- src/Lean/Parser/Term.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 71a3da1b5d..e48c8d90e6 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -191,6 +191,7 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls @[builtinTermParser] def typeOf := leading_parser "typeOf% " >> termParser maxPrec @[builtinTermParser] def ensureTypeOf := leading_parser "ensureTypeOf% " >> termParser maxPrec >> strLit >> termParser @[builtinTermParser] def ensureExpectedType := leading_parser "ensureExpectedType% " >> strLit >> termParser maxPrec +@[builtinTermParser] def noImplicitLambda := leading_parser "noImplicitLambda% " >> termParser maxPrec def namedArgument := leading_parser atomic ("(" >> ident >> " := ") >> termParser >> ")" def ellipsis := leading_parser ".."