From f8ac5d25dd7e22aaf59e5f9067db59ffebf52388 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 Apr 2021 17:14:17 -0700 Subject: [PATCH] feat: add notation for helper elaboration function This similar to `binrel%` but for binary operators. See issue #382 --- src/Lean/Parser/Term.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index f100848810..89a36a091a 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -188,7 +188,8 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls @[builtinTermParser] def noindex := leading_parser "no_index " >> termParser maxPrec -@[builtinTermParser] def binrel := leading_parser "binrel% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec +@[builtinTermParser] def binrel := leading_parser "binrel% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec +@[builtinTermParser] def binop := leading_parser "binop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec @[builtinTermParser] def forInMacro := leading_parser "forIn% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec