From 00ca0dde5c27b634fe959c03fbd1fe48aae9370e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 26 Oct 2022 06:18:52 -0700 Subject: [PATCH] feat: add `unop%` term parser We not to support unary minus at `BinOp.toTree` see #1779 --- src/Lean/Parser/Term.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index c326c994a6..ec695095b1 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -491,6 +491,8 @@ def matchAltsWhereDecls := leading_parser "binop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec @[builtin_term_parser] def binop_lazy := leading_parser "binop_lazy% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec +@[builtin_term_parser] def unop := leading_parser + "unop% " >> ident >> ppSpace >> termParser maxPrec @[builtin_term_parser] def forInMacro := leading_parser "for_in% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec